@@ -15,7 +15,15 @@ boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a
1515boolElim True t e = t
1616boolElim False t e = e
1717
18−||| Defines a predicate on Bool which guarantees that the value is true.
18+||| Ensure that some run-time Boolean test has been performed.
19+|||
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
22+||| fact.
23+|||
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.
1927data so : Bool -> Type where oh : so True
2028
2129instance Uninhabited (so False) where