Safe Haskell	None
Language	Haskell2010

Language.Haskell.Liquid.Equational

Synopsis

type Proof = ()
data QED = QED
(***) :: a -> QED -> Proof
(==.) :: a -> a -> a
eq :: a -> a -> a
(?) :: a -> b -> a
withTheorem :: a -> Proof -> a

Documentation

type Proof = () Source #

Proof is just unit

data QED Source #

Casting expressions to Proof using the "postfix" `*** QED`

Constructors

QED

(***) :: a -> QED -> Proof infixl 2 Source #

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

Equational Reasoning operators | The eq operator is inlined in the logic, so can be used in reflected | functions while ignoring the equality steps.

eq :: a -> a -> a infixl 3 Source #

(?) :: a -> b -> a infixl 3 Source #

Explanations

withTheorem :: a -> Proof -> a Source #

Using proofs as theorems