Re: [isabelle] A (very) short Isabelle/HOL tutorial for the functional programmer

Le 19/10/2015 14:55, Rustom Mody a Ãcrit :
Thanks for that Thomas!
Just one point -- I had to change the fun to primrec... Not sure I
understand why but saw that somewhere and tried

Dear Rustom,

you can define remove using "primrec" since it is a primitive recursive function.

However, you should be able to define it using "fun" since "fun" accepts a superset of functions, including primitive recursive ones.

Thomas Genet
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at

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