[Agda] Pattern-matching operation order

[Nils Anders Danielsson]

On 2010-02-17 15:11, Pierre Boutillier wrote:
> data _<_ : Nat → Nat → Set where
>    LE : ∀ {i} → (d : Nat) → i < (d + i)

> minusSS : ∀ {m n} → m < (ss n) → Nat
> minusSS .{ss n}{n} (LE {ss .n} zz) = {!zz!}
> minusSS a = ?

Agda does not make use of the pattern {ss .n} when checking whether (LE
<whatever>) has type m < ss n. See
http://thread.gmane.org/gmane.comp.lang.agda/1161/focus=1165.

--
/NAD