Re: [isabelle] mutually recursive datatypes with records

Quoting Greg Bronevetsky <greg at>:

> 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"

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 =
         foo |
         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
> automatically.
> -- 
>                              Greg Bronevetsky

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