Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term
- To: mailing-list anonymous <mailing.list.anonymous at gmail.com>
- Subject: Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term
- From: Lawrence Paulson <lp15 at cam.ac.uk>
- Date: Tue, 23 Jul 2019 11:06:42 +0100
- Cc: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- In-reply-to: <CALaF1UJRdYy-eUZprhKB6jfXEP_r9wutjk=eJajPNjK0aAAkYQ@mail.gmail.com>
- References: <CALaF1UJRdYy-eUZprhKB6jfXEP_r9wutjk=eJajPNjK0aAAkYQ@mail.gmail.com>
> On 18 Jul 2019, at 00:11, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
> More specifically, I have the following questions, the second being of
> certain practical significance:
> 1. Is introducing theorems that use differing types for variables with the
> identical names/indexnames is considered to be a bad style, is it
> completely illegal or, perhaps, it is actively exploited by user packages
> that I am not aware of?
I think it’s terrible style, and as your example shows, you have to work quite hard to accomplish this.
> 2. Is it acceptable for the user packages to assume that all variables in
> the theorems that they receive as inputs from the users do not have any
> occurrences of variables with the identical names/indexnames and different
I think so.
This archive was generated by a fusion of
Pipermail (Mailman edition) and