Re: [isabelle] mutual and recursive datatype doubts



datatype
 mytype = typ0 | typ1
and
 typ0 = Zero
and
 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.

Tobias





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