Couple of convenience absurd-related functions were added to Data.So.

Author: buzden

libs/base/Data/So.idr

@@ -12,7 +12,7 @@ module Data.So
 ||| If you find yourself using `So` for something other than primitive types,
 ||| it may be appropriate to define a type of evidence for the property that you
 ||| care about instead.
-data So : Bool -> Type where 
+data So : Bool -> Type where
   Oh : So True
 
 implementation Uninhabited (So False) where
@@ -23,4 +23,14 @@ choose : (b : Bool) -> Either (So b) (So (not b))
 choose True  = Left Oh
 choose False = Right Oh
 
+||| Absurd when you have proof that both `b` and `not b` is true.
+export
+soAbsurd : So b -> So (not b) -> Void
+soAbsurd sb snb with (sb)
+  | Oh = uninhabited snb
+
+||| Transmission between usage of value-level `not` and type-level `Not`.
+export
+soNotToNotSo : So (not b) -> Not (So b)
+soNotToNotSo = flip soAbsurd