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

Le 19/10/2015 15:50, Rustom Mody a Ãcrit :
fun give this error

   remove :: "'a â 'a list â 'a list"
Found termination order: "(Îp. length (snd p)) <*mlex*> {}"

OK, this is not an error. When defining functions with fun, the termination has to be proved (it is not guaranteed by construction like it is for primrec). The output states that the termination has been proven automatically by using a termination order comparing the lenght of the lists of the second argument of the function.

But, true, this should be clarified in the tutorial.


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.