[Agda] Does the order of patterns matter?

[Nils Anders Danielsson]

On 2012-09-27 12:51, Martin Escardo wrote:
> (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.

Currently Agda doesn't have a small trusted core language, but
eventually we may want to move in that direction. This kind of change
could make the core language (or the translation into the core) quite a
bit more complicated.

-- 
/NAD