Re: [isabelle] mutually recursive datatypes with records
Quoting Greg Bronevetsky <greg at bronevetsky.com>:
> Ok, in that case I can replace this record type with a regular tuple, as
> datatype type1 =
> foo |
> bar "type2 list"
> and type2 = "nat * type1"
Your definition is not what you mean, and I didn't realize that before either:
Datatype definitions always start with a constructor after the equals sign.
Apparently Isabelle is very liberal about names here, so it interprets "nat *
type1" as a nullary constructor name, which results in typing errors afterwards...
Your definition goes:
datatype type1 =
bar "type2 list"
and type2 = type2 "nat * type1"
Hope that helps
> 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
> Greg Bronevetsky
This archive was generated by a fusion of
Pipermail (Mailman edition) and