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
you can define remove using "primrec" since it is a primitive recursive
However, you should be able to define it using "fun" since "fun"
accepts a superset of functions, including primitive recursive ones.
Campus de Beaulieu, 35042 Rennes cedex, France
TÃl: +33 (0) 2 99 84 73 44 E-mail: genet at irisa.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and