[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
"(n::real)>0 ==> floor(n) = n"
instead of adding 'real' around the 'floor' I got the output
goal (1 subgoal):
1. (0âreal) < real n ==> âreal nâ = n
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
"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