Re: [isabelle] Type annotations
"[| ALL n1 n2. k n1 = k n2 --> n1 = n2;
k x1 = k x2 |] ==> x1 = x2"
It works because k is inferred to have type 'a => 'b.
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"
It fails because - by restricting the type - you have given the simplifier
the chance for an infinite recursive invocation of the conditional rewrite rule
k n1 = k n2 --> (n1 = n2) = True
This is simply stopped once simp_depth_limit is reached.
This archive was generated by a fusion of
Pipermail (Mailman edition) and