Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Defining a recursive function


view this post on Zulip 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

view this post on Zulip 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: Mar 28 2024 at 20:16 UTC