Re: [isabelle] mutually recursive datatypes with records



Hi Greg,

> I'm trying to create a mutually recursive datatype where one half of it
> is specified via the datatype keyword and the other half via a record 
> keyword.

Records in Isabelle/HOL (like in ML) are always non-recursive, so you really
need a datatype here. If you insist on record-like syntax, you can probably
achieve this by syntax translations.

Alex





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