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.


> On 2 Sep 2015, at 09:59, Lars Hupel <hupel at> 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.