Decidable.Equality

interface DecEq 

Decision procedures for propositional equality

decEq : DecEq t => (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

Decide whether two elements of t are propositionally equal

ZnotS : (0 = S n) -> Void

decEqSelfIsYes : DecEq a => decEq x x = Yes Refl

Everything is decidably equal to itself

leftNotRight : (Left x = Right y) -> Void

lemma_both_neq : ((x = x') -> Void) -> ((y = y') -> Void) -> ((x, y) = (x', y')) -> Void

lemma_fst_neq_snd_eq : ((x = x') -> Void) -> (y = y') -> ((x, y) = (x', y)) -> Void

lemma_snd_neq : (x = x) -> ((y = y') -> Void) -> ((x, y) = (x, y')) -> Void

lemma_val_not_nil : (x :: xs = []) -> Void

lemma_x_eq_xs_neq : (x = y) -> ((xs = ys) -> Void) -> (x :: xs = y :: ys) -> Void

lemma_x_neq_xs_eq : ((x = y) -> Void) -> (xs = ys) -> (x :: xs = y :: ys) -> Void

lemma_x_neq_xs_neq : ((x = y) -> Void) -> ((xs = ys) -> Void) -> (x :: xs = y :: ys) -> Void

negEqSym : ((a = b) -> Void) -> (b = a) -> Void

The negation of equality is symmetric (follows from symmetry of equality)

nothingNotJust : (Nothing = Just x) -> Void

trueNotFalse : (True = False) -> Void