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