[isabelle] Defining a recursive function

Dear Isabelle list,

I am defining a datatype and a recursive function as below:

typedecl Mat

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.

Best regards,
Shuling Wang
SKLCS, Institute of Software, Chinese Academy of Sciences

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