*To*: Gabriele Pozzani <gabriele.pozzani at gmail.com>*Subject*: Re: [isabelle] Sequence case*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Wed, 20 Sep 2006 16:42:32 +0200*Cc*: Isabelle <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <b3262abf0609190641p5f8c6899h5b6e5c3d4b075d73@mail.gmail.com>*References*: <b3262abf0609190641p5f8c6899h5b6e5c3d4b075d73@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.2 (Macintosh/20060308)

So I wrote: consts first_occur::"('a × 'b) lift seq => 'a => 'b" primrec "first_occur ex a == (case ex of x##xs => if (fst(x)=a) then snd(x) else (first_occur xs a) | _ => arbitrary)" But it don't work and Isabelle stops with the follow error: *** exception TERM raised: Error in case expression: *** Not a datatype constructor: Cfun.Rep_CFun *** Error in parse translation for "_case_syntax" *** At command "primrec". Where is the problem?

Tobias

**References**:**[isabelle] Sequence case***From:*Gabriele Pozzani

- Previous by Date: Re: [isabelle] Sequence case
- Next by Date: Re: [isabelle] Simplifier questions
- Previous by Thread: Re: [isabelle] Sequence case
- Next by Thread: [isabelle] Call for Participation: Training School in Symbolic Computation
- Cl-isabelle-users September 2006 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