Decidable.Decidable.Extra

Definitions

NotNot : Rel ts -> Rel ts

Totality: total
Visibility: public export

doubleNegationElimination : Decidable n ts r => (witness : HVect ts) -> uncurry (NotNot r) witness -> uncurry r witness

Totality: total
Visibility: public export

doubleNegationExists : Decidable n ts r => Ex ts (NotNot r) -> Ex ts r

Totality: total
Visibility: public export

negateDec : Dec a -> Dec (Not a)

  Convert a decision about a decidable property into one about its negation.

Totality: total
Visibility: public export

notExistsNotForall : {0 p : a -> Type} -> ((x : a) -> Dec (p x)) -> Dec (x : a ** Not (p x)) -> Dec ((x : a) -> p x)

  We can turn (Not (Exists Not)) into Forall for decidable types

Totality: total
Visibility: public export