Re: [isabelle] primrec or fun
> 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and