git.iko.soy/Idris-dev
on master help sign in
add proof of `decEq x x = Yes Refl`
17eb61cAlex Gryzlov
libs/prelude/Decidable/Equality.idr+15−9
compare with master
unifiedsplit
@@ -8,18 +8,10 @@ import Prelude.Either
8import Prelude.List
8import Prelude.List
9import Prelude.Nat
9import Prelude.Nat
10import Prelude.Maybe
10import Prelude.Maybe
11+import Prelude.Uninhabited
11
12
12%access public export
13%access public export
13
14
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−
23--------------------------------------------------------------------------------
15--------------------------------------------------------------------------------
24-- Decidable equality
16-- Decidable equality
25--------------------------------------------------------------------------------
17--------------------------------------------------------------------------------
@@ -29,6 +21,20 @@ interface DecEq t where
29 ||| Decide whether two elements of `t` are propositionally equal
21 ||| Decide whether two elements of `t` are propositionally equal
30 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
22 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
31
23
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+
32--------------------------------------------------------------------------------
38--------------------------------------------------------------------------------
33--- Unit
39--- Unit
34--------------------------------------------------------------------------------
40--------------------------------------------------------------------------------