Re: [isabelle] primrec or fun

One of the advantages of primrec is that fun generates a number of auxiliary definitions and facts that you may not need for simple recursion patterns like the ones supported by primrec, so primrec is more âlight-weightâ and may be faster.

I therefore tend to use primrec whenever it is possible and I don't need the facts generated by fun.


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