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:

	http://matryoshka.gforge.inria.fr/pubs/bindings.pdf

Cheers,

Jasmin





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