Re: [isabelle] primrec or fun



Joachim wrote:

> There are only a few (obscure?) cases where fun cannot do what primrec
> can, as Andreas writes on SO: When a data type does not have a size
> function.

There's also the case of mutual recursion on mutually defined datatypes, where I've seen some "fun" failures.

"primrec" is more lightweight, so if you develop large theories it might help make Isabelle take fewer resources. *Might* because I'm not aware of any actual measurements.

Jasmin





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