add Uninhabited instances for True=False, remove unused proof from Data.Heap
commit5a2d752d3ae10409b27316026fce27d66caf83ee
authorAlex Gryzlov <alexander.gryzlov@adform.com>
dateTue 18 Jul 2017, 13:07 (9 years ago)
parent8c5de76
libs/contrib/Data/Heap.idr−4
@@ -132,10 +132,6 @@ implementation Ord a => Monoid (MaxiphobicHeap a) where
132132-- Properties
133133--------------------------------------------------------------------------------
134134
135−total
136−absurdBoolDischarge : False = True -> Void
137−absurdBoolDischarge Refl impossible
138−
139135total
140136isEmptySizeZero : (h : MaxiphobicHeap a) -> (isEmpty h = True) -> size h = Z
141137isEmptySizeZero Empty p = Refl
libs/prelude/Prelude/Bool.idr+9
@@ -35,3 +35,12 @@ not : Bool -> Bool
3535not True = False
3636not False = True
3737
38+--------------------------------------------------------------------------------
39+-- Properties
40+--------------------------------------------------------------------------------
41+
42+Uninhabited (True = False) where
43+ uninhabited Refl impossible
44+
45+Uninhabited (False = True) where
46+ uninhabited Refl impossible