qed-0.0: Simple prover

Safe Haskell	None
Language	Haskell98

Proof.QED

Documentation

data QED a Source

Instances

Monad QED Source
Functor QED Source
Applicative QED Source
MonadIO QED Source

qed :: QED a -> IO () Source

imports :: FilePath -> QED () Source

decl :: String -> QED () Source

data Laws Source

Instances

Monoid Laws Source

law :: PropString -> QED Laws Source

laws :: QED a -> QED Laws Source

data Proof a Source

Instances

Monad Proof Source
Functor Proof Source
Applicative Proof Source
MonadThrow Proof Source
MonadCatch Proof Source
MonadMask Proof Source
MonadIO Proof Source

type PropString = String Source

prove :: PropString -> Proof () -> QED () Source

data Bind a Source

Instances

Monad Bind Source
Functor Bind Source
Applicative Bind Source

satisfy :: String -> Laws -> Bind () -> QED () Source

bind :: String -> Bind () Source

rhs :: Proof () -> Proof () Source

lhs :: Proof () -> Proof () Source

bhs :: Proof () -> Proof () Source

at :: Int -> Proof () -> Proof () Source

recurse :: Proof () Source

unfold :: String -> Proof () Source

unfold_ :: Proof () Source

strict :: String -> Proof () Source

expand :: Proof () Source

unlet :: Proof () Source

divide :: Proof () Source

twice :: Proof () -> Proof () Source

thrice :: Proof () -> Proof () Source

many :: Proof () -> Proof () Source

perhaps :: Proof () -> Proof Bool Source

skip :: QED () -> QED () Source

qedCheat :: QED a -> IO () Source

unsafeCheat :: String -> Proof () Source