git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3905 from clayrat/patch-1
05fbd11David Christiansen
CHANGELOG.md+3
compare with master
unifiedsplit
@@ -22,6 +22,9 @@
22 with a (strictly) smaller `size`.
22 with a (strictly) smaller `size`.
23
23
24 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
24 A good example of this idiom at work is `Data.List.Views.splitRec` from `base`.
25++ Added utility lemma `decEqSelfIsYes : decEq x x = Yes Refl` to
26+ `Decidable.Equality`. This is primarily useful for proving properties of
27+ functions defined with the help of `decEq`.
25
28
26## Tool Updates
29## Tool Updates
27
30
libs/prelude/Decidable/Equality.idr+15−9
@@ -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--------------------------------------------------------------------------------