[isabelle] Difference between primrec and fun

Dear all,

Isabelle has different commands for introducing recursive functions: fun, function, primrec.

The relationship between fun and function is clear to me: fun is just a convenience command that invokes function with some useful defaults.

But I cannot figure out what primrec is meant for. From the documentation (isar-ref), primrec does the same as fun, except that it imposes additional limitations on the structure of the recursive function. (And in contrast to the fun/function difference, it is not easier/more compact to write.)

So my question is: Is there any difference between primrec and fun in cases when both can be used? In that case: which command tends to be preferable? Why does primrec exist?

Best wishes,

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