[isabelle] defining records (development version) · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] defining records (development version)

Email Gateway (Aug 18 2022 at 09:55):

From: Michael Norrish <Michael.Norrish@nicta.com.au>
It would be nice if the name of the record package's internal K
combinator (currently "Record.K_record") was available in the
RecordPackage signature, alongside strings such as updateN and
others.

Also, if I have

record inner =
fld1 :: nat
fld2 :: nat

record outer =
fld3 :: inner
fld4 :: nat

it would be nice if

fld3_update (fld1_update (K_record 3)) x

printed more prettily than just the above. I'm afraid I don't have
any good suggestions as to just what should come out though (HOL4
doesn't do anything nice here either).

Something like

x (| fld3.fld1 = 3 |)

would be spiffy, but I don't know if that would work given all the
other constraints on syntax.

Michael.

Email Gateway (Aug 18 2022 at 09:55):

From: Norbert Schirmer <norbert.schirmer@web.de>
Hi Michael,

On Tuesday 14 November 2006 07:24, Michael Norrish wrote:

It would be nice if the name of the record package's internal K
combinator (currently "Record.K_record") was available in the
RecordPackage signature, alongside strings such as updateN and
others.

Done.

x (| fld3.fld1 = 3 |)

would be spiffy, but I don't know if that would work given all the
other constraints on syntax.

Yes this would be nice. Unfortunately there is a conflict with qualified
names. If a bright idea and a bag full of time comes along my way I will
implement some syntax.

Norbert

Email Gateway (Aug 18 2022 at 09:56):