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
> 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)) "

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