Re: [isabelle] Proof of concept: BNF-based records

On 16 Feb 2018, at 07:56, Makarius <makarius at<mailto:makarius at>> wrote:

On 14/02/18 22:12, Gerwin.Klein at<mailto:Gerwin.Klein at> wrote:

I must admit that we have been maintaining a similar (very bare-bones) additional datatype record package on the side for about a decade. We use it in addition to the standard record package to model C structs, because they can contain recursive pointer types, which we couldn’t do with normal records. I.e. it might make sense to have both, as long as it is clear what each is for, what the differences are, and why they can’t/shouldn’t be the same.

Can you point to the sources of this alternative datatype record
package? How does it treat record syntax?

The syntax is a very ad-hoc partial reuse of the standard record translations. Definitely not thought as an example to be followed.


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