[isabelle] size for records



Dear list,

I'm having a lot of troubles with records right now. They're not BNFs,
but luckily there's the "copy_bnf" command. Unfortunately, it seems this
doesn't generate a size function (at least I don't see it). Is it
possible to transfer the size function from the original BNF? Because
without size function, nested recursion through the record becomes tricky.

Cheers
Lars




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