| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
Copilot.Theorem.Prover.SMT
- module Data.Default
- data Options = Options {}
- induction :: SmtFormat a => Options -> Backend a -> Proof Universal
- kInduction :: SmtFormat a => Options -> Backend a -> Proof Universal
- onlySat :: SmtFormat a => Options -> Backend a -> Proof Existential
- onlyValidity :: SmtFormat a => Options -> Backend a -> Proof Universal
- yices :: Backend SmtLib
- dReal :: Backend SmtLib
- altErgo :: Backend SmtLib
- metit :: String -> Backend Tptp
- z3 :: Backend SmtLib
- cvc4 :: Backend SmtLib
- mathsat :: Backend SmtLib
- data Backend a
- class Show a => SmtFormat a
- data SmtLib
- data Tptp
Documentation
module Data.Default
Tactics