[isabelle] exception UnequalLengths raised (line 543 of "library.ML")
I was following along in the case study in tutorial.pdf and I got an
exception while writing my proof. I'm using Isabelle2015 on windows.
Here is a (slightly) simplified version of what I was doing that raised the
example :: "nat set â nat set"
for H :: "nat set"
Inj [intro,simp] : "X â H â X â example H"
| Fst: "X â example H â X â example H"
lemma "G â H â example G â example H"
fix x :: "nat"
assume "G â H â x â example G"
hence "x â example H"
The line "proof(induction)" generates the following:
proof (prove): depth 1
(Gânat set) â (Hânat set) â (xânat) â example G
goal (1 subgoal):
1. x â example H
H :: nat set
x :: nat
exception UnequalLengths raised (line 543 of "library.ML")
Is this a normal error message or does it indicate some problem inside
Isabelle (eg., something I should be reporting)? If you delete the "Fst"
constructor the exception goes away.
This archive was generated by a fusion of
Pipermail (Mailman edition) and