[isabelle] primrec or fun



In
http://stackoverflow.com/questions/30419419/what-is-the-difference-between-primrec-and-fun-in-isabelle-hol
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

Thanks
Rusi



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