Re: [isabelle] simple question



> typedecl sbf
> 
> datatype frm = At sbf | Nt frm
> 
> consts
>   f :: "frm => frm"
>   primrec
>     "f (At x) = At x"
>     "f (Nt x) = Nt(x)"
>     "f (Nt(Nt x)) = f (x)"
> 
> *** Primrec definition error:
> *** illegal argument in pattern
> *** in
> *** "f (Nt (Nt x)) = f x"
> *** At command "primrec".

Primrec does not support nested patterns ("Nt (Nt x)"). Rewrite your
definition or use recdef. Also note that the third pattern is an
instance of the second one, so (if you think of f as a functional
program like in ML), the third equation will never be used...

Alex





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