Idris2Doc : Data.Bool.Decidable

Data.Bool.Decidable

data Reflects : Type -> Bool -> Type
  Totality: total
  Constructors:
  
RTrue : p -> Reflects p True
  
RFalse : Not p -> Reflects p False
invert : (arg : Reflects p b) -> (if b then p else Not p)
  
recompute : Dec a -> (0 _ : a) -> a
  
reflect : (arg : Reflects p b) -> (if c then p else Not p) -> b = c
  
remember : (if b then p else Not p) -> Reflects p b