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