Re: [isabelle] FUN verses PRIMREC



You will not go far wrong if you regard primrec as nothing more than an artefact of the bootstrapping process. Only rarely is it preferable to fun.

You can search the archives at the following URL:

	https://lists.cam.ac.uk/pipermail/cl-isabelle-users/index.html

Larry Paulson


On 8 Jan 2012, at 14:41, Tim Kremann wrote:

> Thank you. However, I am still unclear after reading that thread. Its seems that for the thread example, which goes two levels deep (disallowed for primrec) that fun is the better technique rather than rewriting it to a primitive recursive form. However I have three questions:
> 
> 1) Does using primrec offer any advantages when using certain tactics?
> 
> 2) Why use primrec at all?
> 
> 3) What is the best way to search the archives before posting a question?






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