Re: [isabelle] Instantiation on records



Am 18.11.2013 12:35, schrieb Peter Gammie:
> 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
> ...

Ah, of course. Thank you!

> 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).

Good point. Should've done this.

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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