@@ -8,18 +8,10 @@ import Prelude.Either
88import Prelude.List
99import Prelude.Nat
1010import Prelude.Maybe
11+import Prelude.Uninhabited
1112
1213%access public export
1314
14−--------------------------------------------------------------------------------
15−-- Utility lemmas
16−--------------------------------------------------------------------------------
17−
18−||| The negation of equality is symmetric (follows from symmetry of equality)
19−total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
20−negEqSym p h = p (sym h)
21−
22−
2315--------------------------------------------------------------------------------
2416-- Decidable equality
2517--------------------------------------------------------------------------------
@@ -29,6 +21,20 @@ interface DecEq t where
2921 ||| Decide whether two elements of `t` are propositionally equal
3022 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
3123
24+--------------------------------------------------------------------------------
25+-- Utility lemmas
26+--------------------------------------------------------------------------------
27+
28+||| The negation of equality is symmetric (follows from symmetry of equality)
29+total negEqSym : {a : t} -> {b : t} -> (a = b -> Void) -> (b = a -> Void)
30+negEqSym p h = p (sym h)
31+
32+||| Everything is decidably equal to itself
33+total decEqSelfIsYes : DecEq a => {x : a} -> decEq x x = Yes Refl
34+decEqSelfIsYes {x} with (decEq x x)
35+ | Yes Refl = Refl
36+ | No contra = absurd $ contra Refl
37+
3238--------------------------------------------------------------------------------
3339--- Unit
3440--------------------------------------------------------------------------------