Re: [isabelle] defining records (development version)
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
> 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and