-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Simple prover
--   
--   A prototype proof system.
@package qed
@version 0.0

module Proof.QED.Internal
data Exp
Var :: Var -> Exp
Con :: Con -> Exp
App :: Exp -> Exp -> Exp
Let :: Var -> Exp -> Exp -> Exp
Lam :: Var -> Exp -> Exp
Case :: Exp -> [(Pat, Exp)] -> Exp
data Pat
PCon :: Con -> [Var] -> Pat
PWild :: Pat
newtype Var
V :: String -> Var
[fromVar] :: Var -> String
newtype Con
C :: String -> Con
[fromCon] :: Con -> String
data Prop
Prop :: [Var] -> Exp -> Exp -> Prop
data Side
LHS :: Side
RHS :: Side

-- | All these things are append only
data Known
Known :: [(Var, Exp)] -> [(String, [(Con, Int)])] -> [Prop] -> [Prop] -> Bool -> Known
[definitions] :: Known -> [(Var, Exp)]
[types] :: Known -> [(String, [(Con, Int)])]
[assumed] :: Known -> [Prop]
[proved] :: Known -> [Prop]
[cheater] :: Known -> Bool
getKnown :: QED Known
data Unknown
Unknown :: [Goal] -> Maybe Side -> Int -> Unknown
[goals] :: Unknown -> [Goal]
[focusSide] :: Unknown -> Maybe Side
[focusAt] :: Unknown -> Int
getUnknown :: Proof (Known, Unknown)
data Goal
Goal :: [Prop] -> Prop -> Goal
getGoal :: Proof (Known, Unknown, Goal)
newtype BadProof
BadProof :: String -> BadProof
badProof :: String -> Proof a
isBadProof :: Proof () -> Proof Bool
newtype Laws
Laws :: [Prop] -> Laws

-- | Use a new prop which is the same as the previous goal, but with any
--   number of unfoldings
rewriteUnfold :: Prop -> Proof ()

-- | Use a new prop which is the same as the first goals prop, but with
--   simplified/rearranged expressions
rewriteEquivalent :: Prop -> Proof ()

-- | Apply the coinduction principle on the computation
rewriteRecurse :: Proof ()

-- | Split the expression into multiple subexpressions
rewriteSplit :: Proof ()

-- | The first goal is a tautology
rewriteTautology :: Proof ()

module Proof.QED
data QED a
qed :: QED a -> IO ()
imports :: FilePath -> QED ()
decl :: String -> QED ()
data Laws
law :: PropString -> QED Laws
laws :: QED a -> QED Laws
data Proof a
type PropString = String
prove :: PropString -> Proof () -> QED ()
data Bind a
satisfy :: String -> Laws -> Bind () -> QED ()
bind :: String -> Bind ()
rhs :: Proof () -> Proof ()
lhs :: Proof () -> Proof ()
bhs :: Proof () -> Proof ()
at :: Int -> Proof () -> Proof ()
recurse :: Proof ()
unfold :: String -> Proof ()
unfold_ :: Proof ()
strict :: String -> Proof ()
expand :: Proof ()
unlet :: Proof ()
divide :: Proof ()
twice :: Proof () -> Proof ()
thrice :: Proof () -> Proof ()
many :: Proof () -> Proof ()
perhaps :: Proof () -> Proof Bool
skip :: QED () -> QED ()
qedCheat :: QED a -> IO ()
unsafeCheat :: String -> Proof ()