# [Agda] Does the order of patterns matter?

Martin Escardo m.escardo at cs.bham.ac.uk
Thu Sep 27 12:51:12 CEST 2012

```Nils' message tells us where to find a full explanation of what is going on.

On 27/09/12 11:27, Altenkirch Thorsten wrote:
> The bug is rather that we use the = sign here -
> Epigram avoided this by using |-> and it also kept track of the splittings.

But "|->" would also be wrong, because e.g. in Achim's example, there is
a situation f lhs = rhs where there is no reduction f lhs |-> rhs. But
this is just a notational discussion

Here are some questions/conjectures.

(1) It would be possible to implement Agda so that each equation in a
pattern holds definitionally, if we wished, I believe. Of course, you
would get new definitional equalities not present in Martin-Loef type
theory. But does that matter? Conjecture: no new propositional
equalities arise.

(2) Every equation in a definition by pattern matching should hold
propositionally (we know that this is not the case definitionally).
This should be a meta-theorem.

(3) Is there a nice characterization of pattern-matching definitions
such that every "definining equation" does hold definitionally? The
Berry-function in Nils' response indicates that this may be hard. Such
pattern-system should be invariant under permuting equations, in
suitable sense.

(4) What is there against forcing defining equations to hold
definitionally, other than being able to compile them to
eliminator-trees? Already in definitions by pattern matching on natural
numbers there is a departure from Martin-Lof type theory, because in
MLTT you need an inductive definition to even compute the predecessor
function. So why not go a bit further, provide (1) and (2) make sense?

It is very disturbing that a proof ceases to type check if we reorder
mutually exclusive, complete patterns.

Such an extension should be conservative in the sense of allowing more
proofs, but no new theorems. (Which the eta-rule doesn't satisfy, but
nevertheless we seem to be happy to add.)

Best,
Martin
```