[isabelle] Defining a recursive function
Dear Isabelle list,
I am defining a datatype and a recursive function as below:
comm = Init "nat list" "nat"
| Cond "comm list"
primrec denoFunDef::"commâMatâMat" where
"denoFunDef (Init m n) p=p"|
"denoFunDef (Cond mcl) p = (case mcl of  â p
| ac#la â(denoFunDef ac p)) "
An error âExtra variables on rhs: "denoFunDef"â occurs. I donât know why this occurs since denoFunDef is the recursive function being defined. How should I define the function?
Thanks in advance forsolving my question.
SKLCS, Institute of Software, Chinese Academy of Sciences
This archive was generated by a fusion of
Pipermail (Mailman edition) and