Idris2Doc : Data.Bool.Decidable

Data.Bool.Decidable

Reflects : Type -> Bool -> Type
Totality: total
Constructors:
RTrue : p -> ReflectspTrue
RFalse : Notp -> ReflectspFalse
invert : ({arg:409} : Reflectspb) -> (ifbthenpelseNotp)
recompute : Deca -> (0 _ : a) -> a
reflect : ({arg:460} : Reflectspb) -> (ifcthenpelseNotp) -> b = c
remember : (ifbthenpelseNotp) -> Reflectspb