BasicProof(hs_basic_proof)
|
Result of proving a theory. |
Comorphism(hs_comorphism)
|
A comorphism from one logic to another. |
ConsistencyChecker(hs_cons_checker)
|
A tool to check the consistency of a theory. |
ConservativityChecker(hs_conservativity_checker)
|
|
ConsistencyStatus(hs_cons_status)
|
Consistency status of a node. |
DevelopmentGraph(hs_development_graph, parent)
|
|
DevGraphEdge(hs_edge, parent)
|
|
DefinitionDevGraphEdge(hs_edge, parent)
|
|
TheoremDevGraphEdge(hs_edge, parent)
|
|
EdgeKind(value)
|
An enumeration. |
DevGraphNode(hs_node, parent)
|
|
ReferenceDevGraphNode(hs_node, parent)
|
|
LocalDevGraphNode(hs_node, parent)
|
|
GMorphism(hs_g_morphism)
|
|
GlobalAnnotations(hs_global_annos)
|
|
Library(hs_library)
|
|
load_library(path[, options])
|
|
Logic(name, description)
|
|
ProofState(hs_proof_state, theory)
|
|
ProofDetails(hs_proof_status[, kind])
|
|
ProofKind(value)
|
An enumeration. |
ConsistencyKind(value)
|
A type of consistency of a theory. |
Options(**kwargs)
|
|
Option(name, description, typ, hs_name)
|
|
Prover(hs_prover)
|
|
Sentence(hs_sentence_with_name, hs_pretty_fn)
|
|
Signature(hs_signature)
|
|
Theory(hs_theory, parent)
|
|