Re: [isabelle] mutually recursive datatypes with records




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
Ok, in that case I can replace this record type with a regular tuple, as below:
   datatype type1 =
       foo |
       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 unification error:
"Type unification failed: Clash of types "Types.type2" and "*"".
I don't know how to force Isabelle to perform the unfolding automatically.

--
                            Greg Bronevetsky






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