[isabelle] Defining a recursive function



Dear Isabelle list,

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

typedecl Mat

datatype
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.