[Agda] Does the order of patterns matter?

[Altenkirch Thorsten]

Hi Achim,

basically a pattern in Agda is a proof of exhaustiveness and Agda will
only recognize exhaustive patterns which are produced by splitting a
trivial pattern. Indeed you don't need (and actually you shouldn't) write
patterns yourself but generate them by starting with a trivial pattern like

x ≡ y = { }

and then split it by writing the variable in the shed, e.g. x and typing
C-c C-c.

Btw, I'd think you should only need 4 lines to define equality.

Another remark: the function you define factors through Bool and the
embedding from Bool to Set.

Thorsten

On 26/09/2012 11:51, "Achim Jung" <A.Jung at cs.bham.ac.uk> wrote:

>Hello,
>
>    I am new to Agda and have run into the following problem.
>When defining a term by pattern matching and when those patterns are
>mutually exclusive, then it seems to me that the order in which they
>are listed should not matter. However, while trying to prove a simple
>statement about equality modulo 2 on the natural numbers, I discovered
>a case where it appears to matter a lot, in that for the first
>definition my theorem type-checks whereas for the second it doesn't.
>The attached short Agda code file is very simple and hopefully
>self-explanatory.
>
>    Achim.
>
>PS: I am running version 2.3.0.1 on Ubuntu 12.04.
>
>-------------------------------------------------------------------------
>  Prof Achim Jung			Tel.: (+44) 121 41 44776
>  School of Computer Science		Sec.: (+44) 121 41 42791
>  The University of Birmingham		Fax.: (+44) 121 41 44281
>  Edgbaston				Email: A.Jung at cs.bham.ac.uk
>  BIRMINGHAM, B15 2TT			Web: http://www.cs.bham.ac.uk/~axj
>  England
>-------------------------------------------------------------------------

This message and any attachment are intended solely for the addressee and may contain confidential information. If you have received this message in error, please send it back to me, and immediately delete it.   Please do not use, copy or disclose the information contained in this message or in any attachment.  Any views or opinions expressed by the author of this email do not necessarily reflect the views of the University of Nottingham.

This message has been checked for viruses but the contents of an attachment
may still contain software viruses which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.