Synopsis

# Documentation

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

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

proof operators requiring proof terms

Comparison operators requiring proof terms

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

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

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

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

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

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

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

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

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

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

Proof combinators (are Proofean combinators)

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

Because provide lemmata ? or ∵

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

data QED Source #

Constructors

 QED

type Proof = () Source #

byTheorem :: a -> Proof -> a Source #

castWithTheorem :: a -> b -> b Source #

cast :: b -> a -> a Source #

class Arg a Source #

Function Equality

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

data PAnd a b Source #

Constructors

 PAnd a b

data POr a b Source #

Constructors

 POrLeft a POrRight b