proof-combinators-0.1.0.0: Proof Combinators used in Liquid Haskell for Theorem Proving

Safe HaskellSafe
LanguageHaskell2010

LiquidHaskell.ProofCombinators

Contents

Synopsis

Proof is just the unit type

type Proof = () Source #

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

Proof Construction

trivial :: Proof Source #

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

data QED Source #

p *** QED casts p into a proof

Constructors

QED 

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

Equational Reasoning

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

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

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

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

Using Proofs

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

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