Data.Bool.Decidable

Definitions

data Reflects : Type -> Bool -> Type

Totality: total
Visibility: public export
Constructors:

RTrue : p -> Reflects p True

RFalse : Not p -> Reflects p False

recompute : Dec a -> (0 _ : a) -> a

Visibility: public export

invert : ({arg:910} : Reflects p b) -> (if b then p else Not p)

Visibility: public export

remember : (if b then p else Not p) -> Reflects p b

Visibility: public export

reflect : ({arg:989} : Reflects p b) -> (if c then p else Not p) -> b = c

Visibility: public export