LiquidHaskell.ProofCombinators

Proof is just the unit type

type Proof = ()

Proofs -------------------------------------------------------------------

Proof Construction

trivial :: Proof

Proof construction -------------------------------------------------------

data QED

p *** QED casts p into a proof

Constructors

QED

(***) :: p -> QED -> () infixl 2

Equational Reasoning

(==.) :: a -> a -> a infixl 3

Equational Reasoning -----------------------------------------------------

(==?) :: a -> a -> a infixl 3

(?) :: a -> Proof -> a infixl 3

Using Proofs

withTheorem :: a -> Proof -> a

Using Proofs -------------------------------------------------------------