Re: [isabelle] Variables in locale assumptions
Clearly every instance of a variable in a single formula must have the same type, and it’s natural to expect that every instance in a list of formulas should also have the same type. The alternative would be very confusing for readers, also in informal mathematics.
On 22 Feb 2014, at 09:47, Peter Lammich <lammich at in.tum.de> wrote:
>> It's this type constraint that surprised me. The post by Makarius
>> explains it, but as a user I would prefer to have complete separation.
>> Is there a compelling reason why it's implemented as it is?
> I frequently run into another instance of this problem, when writing
> something like:
> lemma foo:
> "x & y --> x"
> "x = y --> f x = f y"
> Note that foo(2) is: "?x::bool = ?y ...", which is usually not
> what was intended.
This archive was generated by a fusion of
Pipermail (Mailman edition) and