Re: [isabelle] Instantiation on records



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.