*To*: lucas cavalcante <thesupervisar at gmail.com>*Subject*: Re: [isabelle] simple question*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Sun, 05 Aug 2007 11:15:53 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <b4d8f2180708031553k69554d9ck389befdf234b842d@mail.gmail.com>*References*: <b4d8f2180708031553k69554d9ck389befdf234b842d@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.10 (X11/20060911)

> 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

**References**:**[isabelle] simple question***From:*lucas cavalcante

- Previous by Date: Re: [isabelle] simple question
- Next by Date: [isabelle] Extensive case splits
- Previous by Thread: Re: [isabelle] simple question
- Next by Thread: Re: [isabelle] help
- Cl-isabelle-users August 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list