Idris2Doc : Decidable.Decidable.Extra

Decidable.Decidable.Extra

No documentation for Decidable.Decidable.Extra.DecidableComplement
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