[isabelle] recursive record types



Is there any chance the following will come to be allowed by the
record definition package?

----------------------------------------------------------------------
theory foo imports Main
begin


datatype 'a ptr = Ptr nat

record listnode =
  item :: nat
  nextnode :: "listnode ptr"

end

----------------------------------------------------------------------

It'd be annoying to have to make the nextnode field of "unit ptr", and
end up with an Isabelle model that has less type information than the
original C program.

Michael.






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