Language.Haskell.Liquid.ProofCombinators

Documentation

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

(<=:) :: a -> a -> Proof -> a infixl 3

proof operators requiring proof terms

Comparison operators requiring proof terms

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

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

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

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

(<=.) :: OptLEq a r => a -> a -> r infixl 3

(<.) :: OptLess a r => a -> a -> r infixl 3

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

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

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

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

(==>) :: Proof -> Proof -> Proof

Proof combinators (are Proofean combinators)

(&&&) :: Proof -> Proof -> Proof

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

Because provide lemmata ? or ∵

proof :: Int -> Proof

proof goes from Int to resolve types for the optional proof combinators

toProof :: a -> Proof

simpleProof :: Proof

trivial :: Proof

data QED

Constructors

QED

type Proof = ()

byTheorem :: a -> Proof -> a

castWithTheorem :: a -> b -> b

cast :: b -> a -> a

class Arg a

Function Equality

(=*=.) :: Arg a => (a -> b) -> (a -> b) -> (a -> Proof) -> a -> b

data PAnd a b

Constructors

PAnd a b

data POr a b

Constructors

POrLeft a

POrRight b