Re: [isabelle] Instantiation on records



Hi René and Peter,

For records and linorder, you will also have to make unit an instance of linorder (see the discussion in the following thread from October:
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-October/msg00221.html).

Best,
Andreas

On 18/11/13 12:35, Peter Gammie wrote:
René,

On 18/11/2013, at 10:28 PM, René Neumann wrote:

record test =
  bla :: int

instantiation "test" :: linorder
begin -- "yields: Bad type name"

instantiation "test_scheme" :: (unit) linorder
begin -- "yields: Bad type name"

instantiation "(| bla :: int |)" :: linorder
begin -- "yields: Undeclared type constructor"

You want "test_ext". Note it has an extra type parameter to deal with record extension - so you'll need to assume that the extra bit has a linorder constraint (untested):

instantiation "test_ext" :: (linorder) linorder
begin
...

I don't know if it's described anywhere more recently, but the old tutorial did a good job on records.

I guess the other way to figure this sort of thing out is to grep through the AFP (which is what I just did).

cheers
peter





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