| Safe Haskell | Safe |
|---|---|
| Language | Haskell98 |
Language.Haskell.Liquid.ProofCombinators
- (==:) :: a -> a -> Proof -> a
- (<=:) :: a -> a -> Proof -> a
- (<:) :: a -> a -> Proof -> a
- (>:) :: a -> a -> Proof -> a
- (==?) :: ToProve a r => a -> a -> r
- (==.) :: OptEq a r => a -> a -> r
- (<=.) :: OptLEq a r => a -> a -> r
- (<.) :: OptLess a r => a -> a -> r
- (>.) :: OptGt a r => a -> a -> r
- (>=.) :: OptGEq a r => a -> a -> r
- (?) :: (Proof -> a) -> Proof -> a
- (***) :: a -> QED -> Proof
- (==>) :: Proof -> Proof -> Proof
- (&&&) :: Proof -> Proof -> Proof
- (∵) :: (Proof -> a) -> Proof -> a
- proof :: Int -> Proof
- toProof :: a -> Proof
- simpleProof :: Proof
- trivial :: Proof
- data QED = QED
- type Proof = ()
- byTheorem :: a -> Proof -> a
- castWithTheorem :: a -> b -> b
- cast :: b -> a -> a
- class Arg a
- (=*=.) :: Arg a => (a -> b) -> (a -> b) -> (a -> Proof) -> a -> b
- data PAnd a b = PAnd a b
- data POr a b
Documentation
(<=:) :: a -> a -> Proof -> a infixl 3 Source #
proof operators requiring proof terms
Comparison operators requiring proof terms
proof :: Int -> Proof Source #
proof goes from Int to resolve types for the optional proof combinators
simpleProof :: Proof Source #
castWithTheorem :: a -> b -> b Source #