Search.Negation

Definitions

interface Negates : Type -> Type -> Type

  It is much easier to look for positive evidence than it is to look
  for negative evidence. So instead of looking for `Not q`, we may
  want to look for `p` instead

Parameters: p, q
Methods:

toNegation : p -> Not q

Implementations:

Negates (p x) (q x) => Negates (All p xs) (Any q xs)

Negates (p x) (q x) => Negates (Any p xs) (All q xs)

Negates (LT m n) (GTE m n)

Negates (LTE m n) (GT m n)

toNegation : Negates p q => p -> Not q

Totality: total
Visibility: public export