Data.So

Definitions

data So : Bool -> Type

  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.

Totality: total
Visibility: public export
Constructor: 

Oh : So True

Hint: 

Uninhabited (So False)

choose : (b : Bool) -> Either (So b) (So (not b))

  Perform a case analysis on a Boolean, providing clients with a `So` proof

Totality: total
Visibility: export

decSo : (b : Bool) -> Dec (So b)

Totality: total
Visibility: export

eqToSo : b = True -> So b

Totality: total
Visibility: export

soToEq : So b -> b = True

Totality: total
Visibility: export

soToNotSoNot : So b -> Not (So (not b))

  If `b` is True, `not b` can't be True

Totality: total
Visibility: export

soNotToNotSo : So (not b) -> Not (So b)

  If `not b` is True, `b` can't be True

Totality: total
Visibility: export

soAnd : So (a && b) -> (So a, So (Force b))

Totality: total
Visibility: export

andSo : (So a, So b) -> So (a && Delay b)

Totality: total
Visibility: export

soOr : So (a || b) -> Either (So a) (So (Force b))

Totality: total
Visibility: export

orSo : Either (So a) (So b) -> So (a || Delay b)

Totality: total
Visibility: export