-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Proof Combinators used in Liquid Haskell for Theorem Proving
--   
--   Proof Combinators used in Liquid Haskell for Theorem Proving
@package proof-combinators
@version 0.1.0.0

module LiquidHaskell.ProofCombinators

-- | Proofs
--   -------------------------------------------------------------------
type Proof = ()

-- | Proof construction
--   -------------------------------------------------------
trivial :: Proof

-- | p *** QED casts p into a proof
data QED
QED :: QED
(***) :: () => p -> QED -> ()
infixl 2 ***

-- | Equational Reasoning
--   -----------------------------------------------------
(==.) :: a -> a -> a
infixl 3 ==.
(==?) :: a -> a -> a
infixl 3 ==?
(?) :: a -> Proof -> a
infixl 3 ?

-- | Using Proofs
--   -------------------------------------------------------------
withTheorem :: a -> Proof -> a