Re: [isabelle] size for records



> not only that: the record construction is much more efficient than the datatype one. So, basing record on datatype would make the seL4 people with their huge records quite unhappy.

I'm aware of that, but didn't know that the difference is that large.

> Ideally, there should be a plugin infrastructure and a size plugin for records. (Oh, and record should be localized. :) ) But since the workaround of a manual definition is so easy, it is hard to find a volunteer to do this.

A good starting point could be to decouple record syntax from record
definitions. There's no reason why

  datatype foo = Bar (x: nat) (y: nat)

couldn't be treated as a record, including update functions. I'm already
working on a plugin that produces "*_update" functions (this allows for
record update syntax, albeit not construction syntax). The next step
would be to patch Lem to use this instead of records.

Cheers
Lars




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