[isabelle] Difference between primrec and fun
- To: cl-isabelle-users <cl-isabelle-users at lists.cam.ac.uk>
- Subject: [isabelle] Difference between primrec and fun
- From: Dominique Unruh <unruh at ut.ee>
- Date: Wed, 2 Oct 2019 09:32:30 +0300
- User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:60.0) Gecko/20100101 Thunderbird/60.8.0
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and