[isabelle] primrec or fun

the general advice seems to be:

> *From a practitionerâs point of view, primrec is a lower-level tool that
> you usually do not need to worry about, and simply always use fun.*

However when I see examples anywhere I see mostly primrec and not fun
Also I remember seeing somewhere that primrec is preferable since functions
in Isabelle  must be terminating and with fun that proof obligation needs
to be separately dealt with


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