Idris2Doc : Data.So

Data.So

Definitions

dataSo : 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 : SoTrue

Hint: 
Uninhabited (SoFalse)
choose : (b : Bool) ->Either (Sob) (So (notb))
  Perform a case analysis on a Boolean, providing clients with a `So` proof

Totality: total
Visibility: export
decSo : (b : Bool) ->Dec (Sob)
Totality: total
Visibility: export
eqToSo : b=True->Sob
Totality: total
Visibility: export
soToEq : Sob->b=True
Totality: total
Visibility: export
soToNotSoNot : Sob->Not (So (notb))
  If `b` is True, `not b` can't be True

Totality: total
Visibility: export
soNotToNotSo : So (notb) ->Not (Sob)
  If `not b` is True, `b` can't be True

Totality: total
Visibility: export
soAnd : So (a&&b) -> (Soa, So (Force b))
Totality: total
Visibility: export
andSo : (Soa, Sob) ->So (a&& Delay b)
Totality: total
Visibility: export
soOr : So (a||b) ->Either (Soa) (So (Force b))
Totality: total
Visibility: export
orSo : Either (Soa) (Sob) ->So (a|| Delay b)
Totality: total
Visibility: export