Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term
As a general rule, style is a matter of choice. This particular issue does not seem to arise frequently in practice. It is more common in the HOL world, but even there it doesn’t appear to be a source of controversy.
> On 23 Jul 2019, at 21:59, mailing-list anonymous <mailing.list.anonymous at gmail.com> wrote:
> Dear Lawrence Paulson/All,
> Thank you for your reply.
> I believe that it would be useful to explain what you stated in your email
> in the implementation manual. Of course, while it is difficult/impossible
> to introduce new theorems that use variables with the same name and
> different types using Isar commands only, it is very easy to do so via the
> public ML interface, even by mistake. Unless I have missed something, this
> issue does not seem to be covered at all (I believe that the manual merely
> states that the type inference mechanism rejects such cases). Given that
> using the variables with the same name and different types is considered to
> be a 'terrible' style, it makes me wonder why the public ML interface
> permits it at all... are there any use cases or any plans to exploit this
> feature of the logic in the future?
> Thank you
> On Tue, Jul 23, 2019 at 1:06 PM Lawrence Paulson <lp15 at cam.ac.uk> wrote:
>>> 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
>>> 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
>> I think so.
> Please accept my apologies for posting anonymously. This is done to protect
> my privacy. I can make my identity and my real contact details available
> upon request in private communication under the condition that they are not
> to be mentioned on the mailing list.
This archive was generated by a fusion of
Pipermail (Mailman edition) and