Idris2Doc : Decidable.Decidable.Extra

Decidable.Decidable.Extra

NotNot : Rel ts -> Rel ts
  Totality: total
doubleNegationElimination : Decidable n ts r => (witness : HVect ts) -> uncurry (NotNot r) witness -> uncurry r witness
  Totality: total
doubleNegationExists : Decidable n ts r => Ex ts (NotNot r) -> Ex ts r
  Totality: total
negateDec : Dec a -> Dec (Not a)
  Convert a decision about a decidable property into one about its negation.

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

  Totality: total