[Agda] Does the order of patterns matter?

[Altenkirch Thorsten]

On 26/09/2012 12:13, "Martin Escardo" <m.escardo at cs.bham.ac.uk> wrote:

>On 26/09/12 12:04, Altenkirch Thorsten wrote:
>> 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.
>
>But the patterns are recognized as exhaustive in the given example.

Yes, I missed the point. That teaches me not to send mails when I have no
time. Especially to mailing lists (red face)

>
>The relations ≡ and ≡' (both meaning equality modulo 2, not equality)
>have the same definitions, except that the order of the equations are
>different. Because they are mutually exclusive, this shouldn't matter.

I think this is a misinterpretation of pattern matching. In my view it is
really syntactic sugar for case analysis or the use of eliminators.

In the first pattern the case analysis of the inner 2nd argument comes
before the analysis of the 2nd argument.
(If I had more time I could translate the definitions into eliminator
based definitions to clarify this).

One should not create patterns by hand but by splitting (this was the
message in my previous email). Moreover the fact that patterns look like
equations is misleading. The bug is rather that we use the = sign here -
Epigram avoided this by using |-> and it also kept track of the splittings.

Thorsten


>
>Now, this type-checks:
>
>thm : ∀(x y : ℕ) → (x ≡ y) → (succ x ≡ succ y)
>thm x y p = p
>
>But this doesn't:
>
>no-thm : ∀(x y : ℕ) → (x ≡' y) → (succ x ≡' succ y)
>no-thm x y p = p
>
>Why???
>
>Martin
>
>_______________________________________________
>Agda mailing list
>Agda at lists.chalmers.se
>https://lists.chalmers.se/mailman/listinfo/agda


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.