A value "a" that is proven to hold the property "b"

Both "a" and "b" holds

"a" or "b" holds

A negation of a proof

Exlusive or

Implies that if "a" holds than "b" holds

Used by library writers to create axioms with non-exported constructors

Used by library writers to create build a Or proof

Used by library writers to create build a And proof

Used by library writers to create build a Not proof

Basic logic

Basic logic

Basic logic

Basic logic

A convience method to check two proofs

A convience method to check two proofs at once

Basic logic

Basic logic

Basic logic

Basic logic

Extract the actual value and remove the proof

Basic logic

Synonym for "modus ponens"

Basic logic

Synonym for "modus tollens"

Used by library writers to imply proof relations

Used by library writers to carefully ignore "impossible" states