| Copyright | (c) Otto-von-Guericke University of Magdeburg |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Safe Haskell | None |
HetsAPI.InfoCommands
Description
Synopsis
- getGraphForLibrary :: LibName -> LibEnv -> DGraph
- getNodesFromDevelopmentGraph :: DGraph -> [DGNodeLab]
- getLNodesFromDevelopmentGraph :: DGraph -> [LNode DGNodeLab]
- getEdgesFromDevelopmentGraph :: DGraph -> [DGLinkLab]
- getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab]
- getAllSentences :: G_theory -> SentenceByName
- getAllAxioms :: G_theory -> SentenceByName
- getAllGoals :: G_theory -> SentenceByName
- getProvenGoals :: G_theory -> SentenceByName
- getUnprovenGoals :: G_theory -> SentenceByName
- prettySentence :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Sentence -> String
- prettySentenceOfTheory :: G_theory -> Sentence -> String
Documentation
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
getLEdgesFromDevelopmentGraph :: DGraph -> [LEdge DGLinkLab] Source #
getAllGoals :: G_theory -> SentenceByName Source #
prettySentence :: Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => lid -> Sentence -> String Source #
prettySentenceOfTheory :: G_theory -> Sentence -> String Source #