Re: [isabelle] size for records



Hi Jasmin,

> To quote from the docs: "For each datatype t, the size plugin generates a generic size function t.size_t as well as a specific instance size :: t â nat belonging to the size type class."
> 
> The key word is "datatype". In general, a BNF is not a datatype.

yeah, right. I guess the general problem is that records are
insufficiently like datatypes. But rebasing their construction on top of
new datatypes would be a significant effort.

> I would presume that this should be an easy task for the Lifting package. Otherwise, you should be able to define the size function manually without too much effort.

Sure, and I just went down that route (manually). But I thought I might
ask if someone has done anything similar :-)

Cheers
Lars




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