Language.Haskell.Liquid.RTick.Combinators

Documentation

type Proof = ()

data QED

Constructors

QED

ASS

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

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

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

isAss :: QED -> Bool

toProof :: a -> Proof

trivial :: Proof

withTheorem :: a -> Proof -> a

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

Equational:

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

eq :: a -> a -> a

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

Inequational:

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

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

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

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

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

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

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

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

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

(>~>.) :: Tick a -> Tick a -> Tick a infixl 3

(>~>?) :: Tick a -> Tick a -> Tick a infixl 3

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

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

(<~<.) :: Tick a -> Tick a -> Tick a infixl 3

(<~<?) :: Tick a -> Tick a -> Tick a infixl 3

(.<==) :: Tick a -> Int -> Tick a -> Tick a infixl 3

(?<==) :: Tick a -> Int -> Tick a -> Tick a infixl 3

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

Cost separators:

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

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

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

(==!) :: a -> a -> a

assert :: Bool -> Proof

Basic: