[isabelle] Records definitions: mutual + self-referencing



Hey,

I'm trying to create a record "A" which includes a field of type another
record "B". "B" itself contains a field of type "A". Is there a way to
define them mutually as we did in, for example, mutually recursive
datatypes?

record A =
 a : int
 b : B

record B =
 x : int
 y : A

Secondly, how do I define a record which contains a field of type itself:

record Block =
 a : int
 b : Block


(p.s. I know both these example contain syntax errors. They're just to
explain what I'm trying to do.)



--
Nauman ...

Blog: http://recluze.wordpress.com
Group: http://securityengineering.wordpress.com
Art gallery: http://recluse.gfxartist.com
Cell: 0321 90 66 275




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