Re: [isabelle] Nominal2 and exception UnequalLengths raised



> exception UnequalLengths raised (line 519 of "library.ML")


Yes, this is because of nested datatypes (which were not really supported when I and others implemented Nominal). It would be good to have this restriction lifted. I think this is the main obstacle in many use cases.


Christian

________________________________
From: cl-isabelle-users-bounces at lists.cam.ac.uk <cl-isabelle-users-bounces at lists.cam.ac.uk> on behalf of Jasmin Blanchette <jasmin.blanchette at inria.fr>
Sent: 28 March 2018 20:26:47
To: Brian Huffman
Cc: isabelle-users; Mark Wassell
Subject: Re: [isabelle] Nominal2 and exception UnequalLengths raised

Hi Brian,

> On 28. Mar 2018, at 21:09, Brian Huffman <huffman.brian.c at gmail.com> wrote:
>
> I am planning to make a project out of fixing it, and updating
> nominal_datatype to be able to take advantage of all the latest
> datatype package features. (Currently nominal_datatype uses the
> old_datatype command internally.) I'll keep you posted on any
> progress.

I understand this is isabelle-users, but for the record the most recent version of Nominal2's "nominal_datatype" (since AFP/9dbda7f8b6c4, 2 Jan 2018) builds a new (BNF-style) datatype instead of an "old" datatype, and "old_datatype" has been discontinued (since Isabelle/0ee38196509e, 2 Jan 2018). But beyond that, I'm not sure we're really "taking advantage" of the latest datatype package features. What do you have in mind specifically? Nested nominal datatypes? Incidentally, see also this draft:

        https://emea01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmatryoshka.gforge.inria.fr%2Fpubs%2Fbindings.pdf&data=01%7C01%7Cchristian.urban%40kcl.ac.uk%7Cb7b6b56183954cd0d1c208d594e1f0ef%7C8370cf1416f34c16b83c724071654356%7C0&sdata=IiXSRwgWzFGosudD9T8U2NaX90DJ6j4n3JtGx5j%2BMUI%3D&reserved=0

Cheers,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.