*To*: Makarius <makarius at sketis.net>*Subject*: Re: [isabelle] function with non-linear patterns*From*: Alexander Krauss <krauss at in.tum.de>*Date*: Mon, 14 May 2012 23:39:03 +0200*Cc*: isabelle-users at cl.cam.ac.uk, trung tran nguyen <ntrtrung at gmail.com>*In-reply-to*: <alpine.LNX.2.00.1205141923310.3781@macbroy21.informatik.tu-muenchen.de>*References*: <alpine.LNX.2.00.1205081143140.15872@macbroy21.informatik.tu-muenchen.de> <CAGxybBVf9oNkeNSjZSXJz=YqOW6sAETqkwUaP7jZ87VP-GKWNg@mail.gmail.com> <alpine.LNX.2.00.1205141923310.3781@macbroy21.informatik.tu-muenchen.de>*User-agent*: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.9.1.16) Gecko/20120320 Icedove/3.0.11

On 05/14/2012 07:29 PM, Makarius wrote:

On Mon, 14 May 2012, trung tran nguyen wrote:function contains ::"'a seq => 'a => bool" where "contains Empty x = False" |"contains (Seq x xs) x = True" |"contains (Seq y xs) x = contains(xs) x" apply pat_completenessexception THM 1 raised (line 334 of "drule.ML"):

[...]

Is there anything fundamentally wrong with the idea of such non-linear function patterns?

Alex

**Follow-Ups**:**Re: [isabelle] function with non-linear patterns***From:*Makarius

**References**:**[isabelle] function with non-linear patterns***From:*Makarius

- Previous by Date: [isabelle] Case distinction with Recursion Induction
- Next by Date: Re: [isabelle] Isabelle on OpenBSD?
- Previous by Thread: [isabelle] function with non-linear patterns
- Next by Thread: Re: [isabelle] function with non-linear patterns
- Cl-isabelle-users May 2012 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