Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Instantiation on records

view this post on Zulip Email Gateway (Aug 19 2022 at 12:32):

From: René Neumann <rene.neumann@in.tum.de>
Dear all,

I'm currently struggeling with making record-types an instance of some
class. I can't find a way of getting hold of the underlying type:

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"

Is it somehow possible to do this? Or should I use explicit 'datatype'
or tuple constructions instead?

Thanks,

view this post on Zulip Email Gateway (Aug 19 2022 at 12:33):

From: Peter Gammie <peteg42@gmail.com>
René,

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

view this post on Zulip Email Gateway (Aug 19 2022 at 12:33):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 12:33):

From: René Neumann <rene.neumann@in.tum.de>
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.

Last updated: Apr 25 2024 at 12:23 UTC