TypeLevel.Bool

Rebinable syntax helper.

Documentation

ifThenElse :: The Bool c -> ((c :~: True) -> a) -> ((c :~: False) -> a) -> a

For use with -XRebindableSyntax. This function can be used to make Haskell look reasonably dependent:

depHask :: The Bool x -> IfThenElse x Int String
depHask cond =
    if cond
        then \Refl -> 1
        else \Refl -> "abc"

type family IfThenElse (c :: Bool) (true :: k) (false :: k) :: k where ...

Type-level if then else.

Equations

IfThenElse True true false = true

IfThenElse False true false = false