Re: [isabelle] mutual and recursive datatype doubts

 mytype = typ0 | typ1
 typ0 = Zero
 typ1 = One

does not do what you think it does, neither in Isabelle nor in ML.
The above declares mytype to be a type with two nullary constructors typ0 and typ1. (The name space for types and functions is disjoint.) There are no untagged union types in the ML family of languages, incl HOL.


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