Idris2Doc : Decidable.Decidable.Extra

Decidable.Decidable.Extra

NotNot : Relts -> Relts
Totality: total
doubleNegationElimination : Decidablentsr => (witness : HVectts) -> uncurry (NotNotr) witness -> uncurryrwitness
Totality: total
doubleNegationExists : Decidablentsr => Exts (NotNotr) -> Extsr
Totality: total
negateDec : Deca -> Dec (Nota)
  Convert a decision about a decidable property into one about its negation.

Totality: total
notExistsNotForall : {0 p : a -> Type} -> ((x : a) -> Dec (px)) -> Dec (DPaira (\x => Not (px))) -> Dec ((x : a) -> px)
  We can turn (Not (Exists Not)) into Forall for decidable types

Totality: total