| Copyright | (c) Rainer Grabbe |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | Christian.Maeder@dfki.de |
| Stability | provisional |
| Portability | needs POSIX |
| Safe Haskell | None |
THF.ProverState
Description
Data structures, initialising functions for Prover state and configurations.
Documentation
data ProverStateTHF Source #
Constructors
| ProverStateTHF | |
Fields
| |
initialProverStateTHF :: SignTHF -> [Named THFFormula] -> [FreeDefMorphism THFFormula MorphismTHF] -> ProverStateTHF Source #
showProblemTHF :: ProverStateTHF -> Named THFFormula -> [String] -> IO String Source #
getAxioms :: ProverStateTHF -> [String] Source #
thfAxioms :: [FormulaRole] Source #