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 in.tum.de> wrote:
> I reckon you want the variable "n" to be of type "real". In that case, use
> a "fixes" declaration:
> fixes n :: real
> shows "n>0 ==> floor(n) = n"
This archive was generated by a fusion of
Pipermail (Mailman edition) and