[isabelle] strange type inference



so far in my experiments Isabelle was able to infer types correctly, and
even to place conversion functions when necessary (such as 'real' to
convert nats and ints to reals when necessary.) but in the following
example,

    declare [[show_types]]
    lemma
      "(n::real)>0 ==> floor(n) = n"
    oops

instead of adding 'real' around the 'floor' I got the output

    goal (1 subgoal):
     1. (0âreal) < real n ==> âreal nâ = n
    variables:
      n :: int

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. I was able to get what
I wanted by changing the lemma to

    lemma
      "n>0 ==> floor(n) = (n::real)"

but I'd like to know in general at what situations can type constraints be
ignored, and if there's a way to get a clear message when it happens.




-- 
I can't see very far,
I must be standing on the shoulders of midgets.



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