@@ -15,7 +15,15 @@ boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
15boolElim True t e = t
15boolElim True t e = t
16boolElim False t e = e
16boolElim False t e = e
18−||| Defines a predicate on Bool which guarantees that the value is true.
18+||| Ensure that some run-time Boolean test has been performed.
20+||| This lifts a Boolean predicate to the type level. See the function `choose`
21+||| if you need to perform a Boolean test and convince the type checker of this
24+||| If you find yourself using `so` for something other than primitive types,
25+||| it may be appropriate to define a type of evidence for the property that you
26+||| care about instead.
19data so : Bool -> Type where oh : so True
27data so : Bool -> Type where oh : so True
21instance Uninhabited (so False) where
29instance Uninhabited (so False) where