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.

Larry Paulson


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. 
> 
> 
> --
>  Peter
> 
> 
> 





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