Data.Rel.Complement

Definitions

complement : Rel ts -> Rel ts

  The logical complement of a relation.

Totality: total
Visibility: public export

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
Visibility: public export