mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-18 08:42:11 +03:00
26 lines
762 B
Idris
26 lines
762 B
Idris
|
module Data.So
|
||
|
|
|
||
|
|
||| Ensure that some run-time Boolean test has been performed.
|
||
|
|
|||
|
||
|
|
||| This lifts a Boolean predicate to the type level. See the function `choose`
|
||
|
|
||| if you need to perform a Boolean test and convince the type checker of this
|
||
|
|
||| fact.
|
||
|
|
|||
|
||
|
|
||| 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.
|
||
|
|
public export
|
||
|
|
data So : Bool -> Type where
|
||
|
|
Oh : So True
|
||
|
|
|
||
|
|
export
|
||
|
|
implementation Uninhabited (So False) where
|
||
|
|
uninhabited Oh impossible
|
||
|
|
|
||
|
|
||| Perform a case analysis on a Boolean, providing clients with a `So` proof
|
||
|
|
export
|
||
|
|
choose : (b : Bool) -> Either (So b) (So (not b))
|
||
|
|
choose True = Left Oh
|
||
|
|
choose False = Right Oh
|
||
|
|
|