2016-08-04 09:01:25 UTC
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 <***@gmail.com>
Sent: 04 August 2016 09:28:23
To: email@example.com; 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?