Re: [isabelle] Nominal2 Errors in simple datatype declarations
This is because you declare A to have a pair-type. It should
work if you say
... = A name B
and it should have the same effect, except that you do not
A x b
Hope this helps,
PS: I am on vacation until next week...if more problems crop up,
I might not be very quick with responding, but I try to keep an
eye on my email.
From: Edward Pierzchalski <e.a.pierzchalski at gmail.com>
Sent: 04 August 2016 09:28:23
To: cl-isabelle-users at lists.cam.ac.uk; Urban, Christian
Subject: 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