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