Re: [isabelle] Defining a recursive function
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
Just replace "primrec" by "fun", and everything works.
On Do, 2015-10-01 at 08:59 +0000, çæç wrote:
> 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)) "
This archive was generated by a fusion of
Pipermail (Mailman edition) and