Logic.NegClasses

Algebraic properties

class Irreflexive r where

A binary relation R is irreflexive if, for all x, R(x, x) is false. The Irreflexive r typeclass provides a single method, irrefl :: Proof (Not (r x x)), proving the negation of R(x, x) for an arbitrary x.

Within the module where the relation R is defined, you can declare R to be irreflexive with an empty instance:

-- Define an irreflexive binary relation
newtype DifferentColor p q = DifferentColor Defn
type role DifferentColor nominal nominal
instance Irreflexive DifferentColor

Minimal complete definition

Nothing

Methods

irrefl :: Proof (Not (r x x))

class Antisymmetric c where

A binary relation R is antisymmetric if, for all x and y, when R(x, y) is true, then R(y, x) is false. The Antisymmetric typeclass provides a single method, antisymmetric :: r x y -> Proof (Not (r y x)), proving the implication "R(x, y) implies the negation of R(y, x)".

Within the module where R is defined, you can declare R to be antisymmetric with an empty instance:

-- Define an antisymmetric binary relation
newtype AncestorOf p q = AncestorOf Defn
type role DifferentColor nominal nominal
instance Antisymmetric AncestorOf

Minimal complete definition

Nothing

Methods

antisymmetric :: Proof (c p q) -> Proof (Not (c q p))