Re: [isabelle] Fun vs Primrec: difference?

OK, thanks Christian, found something via your link.

P.S. I am using this list via a Usenet reader, and I have not imported all of the old messages when I suscribed to That's the reason why I could not know.

Le Sun, 29 Jul 2012 07:11:59 +0200, Christian Sternagel <c-sterna at> a écrit:

Dear Yannick,

this is not the first time this question is asked. Maybe it is best to read through the previous discussions and come back if still questions remain:

Search for "fun primrec" here:



On 07/29/2012 03:33 AM, Yannick Duchêne (Hibou57) wrote:
Hi people out there,

New beginner here, and so beginner's questions :-P

My first one: what's the difference between “fun” and “primrec” please ?
Both looks similar or synonymous, but surprisingly, when Main is not
imported (yes, I know it should, but that's for testing), “fun” seems
not available.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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