Re: [isabelle] strange type inference



Hello,

> the type inference went against an explicit type constraint 'n::real'.
> this
> was very surprising, since I expected that if Isabelle thinks it can't
> satisfy the constraint it'd issue an error message.

the system decidedly did not go against the explicit type constraint.
However, it applied the coercion _inside_ the type constraint.

A type constraint inside a term can be attached to any term, not just
variables. To illustrate the point, your annotation could also be written
as "(n)::real". The system is free to apply a coercion inside the
parentheses.

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

I admit that it is somewhat unintuitive that the outer syntax "::" has a
different meaning than the inner syntax "::".

Cheers
Lars




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