Data.Bool.Decidable(source)

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:905} : 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:984} : Reflects p b) -> (if c then p else Not p) -> b = c

Visibility: public export