git.iko.soy/Idris-dev
on master help sign in
Merge pull request #3925 from clayrat/move-bool-absurd
aee5b54David Christiansen
libs/contrib/Data/Heap.idr−4
compare with master
unifiedsplit
@@ -132,10 +132,6 @@ implementation Ord a => Monoid (MaxiphobicHeap a) where
132-- Properties
132-- Properties
133--------------------------------------------------------------------------------
133--------------------------------------------------------------------------------
134
134
135−total
136−absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge Refl impossible
138−
139total
135total
140isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141isEmptySizeZero Empty p = Refl
137isEmptySizeZero Empty p = Refl
libs/prelude/Prelude/Bool.idr+9
@@ -35,3 +35,12 @@ not : Bool -> Bool
35not True = False
35not True = False
36not False = True
36not False = True
37
37
38+--------------------------------------------------------------------------------
39+-- Properties
40+--------------------------------------------------------------------------------
41+
42+Uninhabited (True = False) where
43+ uninhabited Refl impossible
44+
45+Uninhabited (False = True) where
46+ uninhabited Refl impossible