*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Question on sequential pattern matching*From*: Yannick Duchêne (Hibou57) <yannick_duchene at yahoo.fr>*Date*: Mon, 30 Dec 2013 01:27:02 +0100*Organization*: Ada @ Home*References*: <4A70972E-B8DA-432E-BE00-D2B38FA6210E@kestrel.edu>*User-agent*: Opera Mail/12.16 (Linux)

In the following artificial example datatype T = A | B | C fun f :: "T ⇒ T ⇒ bool" where "f A A ⟷ True" | "f B B ⟷ True" | "f C C ⟷ True" | "f _ _ ⟷ False" ‘fun’ gives a warning about duplicate rewrite rules Ignoring duplicate rewrite rule: f C B ≡ False Ignoring duplicate rewrite rule: f B C ≡ False Ignoring duplicate rewrite rule: f C B ≡ False Ignoring duplicate rewrite rule: f B C ≡ False

[…] Rephrasing as fun f :: "T ⇒ T ⇒ bool" where "f A A ⟷ True" | "f A _ ⟷ False" | "f B B ⟷ True" | "f B _ ⟷ False" | "f C C ⟷ True" | "f C _ ⟷ False" avoids the issue but is more verbose.

fun f :: "T ⇒ T ⇒ bool" where "f x y ⟷ x = y" Then… thm f.simps …just says: f ?x ?y = (?x = ?y) -- “Syntactic sugar causes cancer of the semi-colons.” [1] “Structured Programming supports the law of the excluded muddle.” [1] [1]: Epigrams on Programming — Alan J. — P. Yale University

**Follow-Ups**:**Re: [isabelle] Question on sequential pattern matching***From:*Alessandro Coglio

**References**:**[isabelle] Question on sequential pattern matching***From:*Alessandro Coglio

- Previous by Date: [isabelle] Question on sequential pattern matching
- Next by Date: Re: [isabelle] A problem on ML-like function programming
- Previous by Thread: [isabelle] Question on sequential pattern matching
- Next by Thread: Re: [isabelle] Question on sequential pattern matching
- Cl-isabelle-users December 2013 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