20070606-1

The order of clauses matters, even in case of disjointness.

Attach:ClauseOrder.agda

  module ClauseOrder where

  -- booleans

  data Bool : Set where
      true  : Bool
      false : Bool

  -- logical T/F
  data  False : Prop where
  record True : Prop where

  triv : True
  triv = record {} 

  T : Bool -> Prop
  T true  = True
  T false = False

  -- natural numbers

  data Nat : Set where
    Zero : Nat
    Succ : Nat -> Nat

  -- less than

  _<_ : Nat -> Nat -> Bool
  Zero   < Succ m = true
  Succ n < Succ m = n < m
  _ < Zero = false

  wk< : forall {n m} -> T (n < m) -> T (n < Succ m)
  wk< {n} {Zero} ()
  wk< {Zero} {_} p = triv  
  wk< {Succ n} {Succ m} p = wk< {n} {m} p

This fails in the emptyness checker, however the following modification succeeds:

  _<_ : Nat -> Nat -> Bool
  _ < Zero = false
  Zero   < Succ m = true
  Succ n < Succ m = n < m

From the user perspective, this is a bug.

Again, here it would be helpful to see how Agda "understood" the original patterns. See Print Reconstructed Terms.

Ulf: This is not a bug, it's just that the user has the wrong idea about what's going on. See Docs.Pattern Matching.