Idris2Doc : Data.Rel.Complement

Data.Rel.Complement

complement : Rel ts -> Rel ts
  The logical complement of a relation.

  Totality: total
notToComplement : (p : Rel ts) -> (elems : HVect ts) -> Not (uncurry p elems) = uncurry (complement p) elems
  The negation of a relation for some elements
  is equal to the complement of the relation.

  Totality: total