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 gmane.science.mathematics.logic.isabelle.user. That's the reason why I could not know.

Le Sun, 29 Jul 2012 07:11:59 +0200, Christian Sternagel <c-sterna at jaist.ac.jp> 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:

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

cheers

chris

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.