Re: [isabelle] mutually recursive datatypes with records
Ok, in that case I can replace this record type with a regular tuple, as
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.
datatype type1 =
bar "type2 list"
and type2 = "nat * type1"
However, now I'm running into another problem: whever I use type2
Isabelle refuses to recognize that its a pair type and whenever I use it
in another type where I use it as a pair, I get the following
"Type unification failed: Clash of types "Types.type2" and "*"".
I don't know how to force Isabelle to perform the unfolding automatically.
This archive was generated by a fusion of
Pipermail (Mailman edition) and