Re: [isabelle] On the status of occurrences of variables with identical names/indexnames and different types in the same context/theorem/term

> On 18 Jul 2019, at 00:11, mailing-list anonymous <mailing.list.anonymous at> 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
> types?

I think so.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.