smtlib2-1.0: A type-safe interface to communicate with an SMT solver.

Safe HaskellNone
LanguageHaskell98

Language.SMTLib2.Internals.Proof

Documentation

data ProofResult e Source

Constructors

ProofExpr (e BoolType) 
EquivSat (e BoolType) (e BoolType) 

Instances

data Proof r e p Source

Constructors

Rule r [p] (ProofResult e) 

verifyProof :: (Monad m, Ord p, Show r, Show p) => (p -> m (Proof r e p)) -> (r -> [ProofResult e] -> ProofResult e -> ExceptT String m ()) -> p -> StateT (Map p (ProofResult e)) (ExceptT String m) (ProofResult e) Source

renderProof :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> m ShowS Source

renderProof' :: (Monad m, Ord p, Show r) => (forall tp. e tp -> ShowS) -> (p -> m (Proof r e p)) -> p -> StateT (Map p Int) (WriterT (Endo String) m) Int Source

renderProofResult :: (forall tp. e tp -> ShowS) -> ProofResult e -> ShowS Source