Re: [isabelle] List construction



Second question: if I don't use unit and () in the definition of the
function, why Isabelle return the error:
*** Primrec definition error:
*** constructor missing
*** in
*** "emptyRes2aux (k::nat) = (case k of 0 => [] | Suc (h::nat) => free #
emptyRes2aux h)"
*** At command "primrec".
?

Isabelle complains about missing constructors because the constructors 0/Suc should occur on the lhs. Please read the description and the many examples of primrec in the tutorial.

Tobias





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