[isabelle] List construction



Hello,
I'm writing a function to contruct a list of given length.

I defined a datatype:
datatype resource = free | taken

and the function:
emptyRes2aux :: "unit => nat => resource list"
primrec
"emptyRes2aux () (k) = (case k of 0 => [] | Suc h => free # emptyRes2aux ()
h)"

The first question is: why now Isabelle give me the error:
*** Constant to be defined occurs on rhs
*** The error(s) above occurred in definition "emptyRes2aux_unit_def":
***   "emptyRes2aux == unit_rec (nat_case [] (h::nat. free # emptyRes2aux ()
h))"
*** At command "primrec".
?

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".
?

Thanks

Gabriele




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