Re: [isabelle] recursive record types



Hi Michael,

On Wednesday 29 November 2006 23:12, Michael Norrish wrote:
> Is there any chance the following will come to be allowed by the
> record definition package?

Such a change is not planned since recursion and extensibility of records 
doesn't seem to fit together too well.

If you really need recursion you can still use a datatype.

> ----------------------------------------------------------------------
> theory foo imports Main
> begin
>
>
> datatype 'a ptr = Ptr nat
>
> record listnode =
>   item :: nat
>   nextnode :: "listnode ptr"
>
> end
>
> ----------------------------------------------------------------------

However, in your example you only want to maintain a kind of type-tag for
"ptr". Maybe one of the following workarounds can still help you:

1)
-------------------------------
datatype 'a ptr = Ptr nat

typedecl listnodeT
record listnode =
  item :: nat
  nextnode :: "listnodeT ptr"
-----------------------------------

------------------------------------
2)
record 'a listnode =
  item ::nat
  nextnode :: "'a ptr"

term "r::(unit listnode) listnode"
---------------------------------------

   Norbert





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