Re: [isabelle] strange type inference



I just want to stress this point: “fixes” is a much better way to constrain the type of a variable. It can also make your theorem statements more legible, even in cases where type inference does the right thing.

Larry

> On 2 Sep 2015, at 09:59, Lars Hupel <hupel at in.tum.de> wrote:
> 
> I reckon you want the variable "n" to be of type "real". In that case, use
> a "fixes" declaration:
> 
>  lemma
>    fixes n :: real
>    shows "n>0 ==> floor(n) = n"
>  oops
> 





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