Hets - the Heterogeneous Tool Set

Copyright(c) Rainer Grabbe
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityneeds POSIX
Safe HaskellNone

THF.ProverState

Description

Data structures, initialising functions for Prover state and configurations.

Documentation

data ProverStateTHF

Constructors

ProverStateTHF 

Fields

axioms :: [Named THFFormula]
 
signature :: SignTHF
 
freeDefs :: [FreeDefMorphism THFFormula MorphismTHF]
 

initialProverStateTHF :: SignTHF -> [Named THFFormula] -> [FreeDefMorphism THFFormula MorphismTHF] -> ProverStateTHF

insertSentenceTHF :: ProverStateTHF -> Named THFFormula -> ProverStateTHF

showProblemTHF :: ProverStateTHF -> Named THFFormula -> [String] -> IO String

getAxioms :: ProverStateTHF -> [String]

thfAxioms :: [FormulaRole]