Re: [isabelle] Nominal2 Errors in simple datatype declarations
Yes, unfortunately things like
nominal_datatype A = A "(name * B) list"
do not work with nominal_datatype and you would have to
implement such terms with your own "copy" of lists.
On Thursday, August 4, 2016 at 09:49:48 (+0000), Edward Pierzchalski wrote:
> Hi Christian,
> That indeed works. However, this came up because originally I was
> trying to declare something like
> nominal_datatype A = A "(name * B) list"
> and B = B nat
> Which throws the same exception. I can get around this as well by
> defining "A" similarly to a list, and indeed that's the solution used
> in "Nominal/Ex/Lambda.thy:24", but I'd prefer to be able to use other
> datatypes in my definitions (redefining "'a set", for instance,
> wouldn't be quite as easy...).
> On Thu, 4 Aug 2016 at 18:58 Urban, Christian
> <christian.urban at kcl.ac.uk> wrote:
> 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)
> 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:
> theory Test
> imports Main "Nominal/Nominal2"
> atom_decl name
> 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?
> 1. mailto:christian.urban at kcl.ac.uk
> 2. mailto:e.a.pierzchalski at gmail.com
> 3. mailto:cl-isabelle-users at lists.cam.ac.uk
This archive was generated by a fusion of
Pipermail (Mailman edition) and