[isabelle] Nominal2 Errors in simple datatype declarations
Hi, I'm getting some mysterious issues using the Nominal2 package. In the
following minimal example:
imports Main "Nominal/Nominal2"
nominal_datatype A = A "(name * B)"
and B = B nat
I get an "UnequalLengths" exception raised by line 544 of "library.ML"
which defines list zip ("~~"). Unfortunately, I don't know how to get stack
traces out of Isabelle theory runs. Any ideas on what's going on?
This archive was generated by a fusion of
Pipermail (Mailman edition) and