Email Gateway (Aug 22 2022 at 11:41): Email Gateway (Aug 22 2022 at 11:41):From: 王淑灵 <wangsl@ios.ac.cn>
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
Email Gateway (Aug 22 2022 at 11:42):From: Peter Lammich <lammich@in.tum.de>
In Isabelle 2015 I get
Invalid map function in "case_list p
(λac la. denoFunDef ac p)"
This indicates that your recursion scheme is outside of what primrec can
do.
Just replace "primrec" by "fun", and everything works.
Last updated: Nov 21 2024 at 12:39 UTC