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
--
Thomas Genet
ISTIC/IRISA
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
http://www.irisa.fr/celtique/genet




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