Re: [isabelle] primrec

That's precisely the point. There are very few reasons to prefer primrec to fun. The latter will also give you an induction rule exactly tailored to your function, and other benefits.

Larry Paulson

On 9 Nov 2011, at 08:21, Viorel Preoteasa wrote:

> Using fun instead of primrec seem to solve the problem,
> but fun seems more general.

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