Re: [isabelle] Nominal2 and exception UnequalLengths raised



On Wed, Mar 28, 2018 at 12:32 AM, Mark Wassell <mpwassell at gmail.com> wrote:
> I am attempting to define programming language case statements in Nominal2
> and get
>
> exception UnequalLengths raised (line 519 of "library.ML")

Hi Mark,

I also came across the same "UnequalLengths" error for exactly the
same reason; I just wrote to Christian Urban this morning about it. 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.

- Brian




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