gdp-0.0.0.2: Reason about invariants and preconditions with ghosts of departed proofs.

Copyright(c) Matt Noonan 2018
LicenseBSD-style
Maintainermatt.noonan@gmail.com
Portabilityportable
Safe HaskellNone
LanguageHaskell2010

Logic.NegClasses

Contents

Description

 

Synopsis

Algebraic properties

class Irreflexive r where Source #

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
instance Irreflexive DifferentColor

Methods

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

irrefl :: Defining (r x x) => Proof (Not (r x x)) Source #

class Antisymmetric c where Source #

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
instance Antisymmetric AncestorOf

Methods

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

antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p)) Source #