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

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.

Page last modified on June 06, 2007, at 05:53 PM

Powered by
PmWiki