Copyright | (c) Otto-von-Guericke University of Magdeburg |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Safe Haskell | None |
Synopsis
- automatic :: LibName -> LibEnv -> LibEnv
- globalSubsume :: LibName -> LibEnv -> LibEnv
- globalDecomposition :: LibName -> LibEnv -> LibEnv
- localInference :: LibName -> LibEnv -> LibEnv
- localDecomposition :: LibName -> LibEnv -> LibEnv
- compositionProveEdges :: LibName -> LibEnv -> LibEnv
- conservativity :: LibName -> LibEnv -> LibEnv
- automaticHideTheoremShift :: LibName -> LibEnv -> LibEnv
- theoremHideShift :: LibName -> LibEnv -> Result LibEnv
- computeColimit :: LibName -> LibEnv -> Result LibEnv
- normalForm :: LibName -> LibEnv -> Result LibEnv
- triangleCons :: LibName -> LibEnv -> Result LibEnv
- freeness :: LibName -> LibEnv -> Result LibEnv
- libFlatImports :: LibName -> LibEnv -> Result LibEnv
- libFlatDUnions :: LibName -> LibEnv -> Result LibEnv
- libFlatRenamings :: LibName -> LibEnv -> Result LibEnv
- libFlatHiding :: LibName -> LibEnv -> Result LibEnv
- libFlatHeterogen :: LibName -> LibEnv -> Result LibEnv
- qualifyLibEnv :: LibName -> LibEnv -> Result LibEnv
- loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv))
- getGraphForLibrary :: LibName -> LibEnv -> DGraph
- getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
- getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
- getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)]
- proveNode :: G_theory -> ProofOptions -> ResultT IO ProofResult
Documentation
loadLibrary :: FilePath -> HetcatsOpts -> IO (Result (LibName, LibEnv)) Source #
getGraphForLibrary :: LibName -> LibEnv -> DGraph Source #
getDevelopmentGraphByName name env
returns the development graph for the
library name
in the environment env
.
getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab] Source #
getNodesFromDevelopmentGraph graph
returns the nodes of the development
graph graph
getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab] Source #
getNodesFromDevelopmentGraph graph
returns the nodes of the development
graph graph
getUsableProvers :: G_theory -> IO [(G_prover, AnyComorphism)] Source #
getUsableProvers theory
checks for usable provers available on the machine