Merge pull request #3925 from clayrat/move-bool-absurd
Add Uninhabited instances for True=False
commitaee5b546772c41c442e08d39a939a55414c8b4bb
authorDavid Christiansen <david@davidchristiansen.dk>
dateTue 18 Jul 2017, 10:02 (9 years ago)
parent8c5de765a2d752
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