Up
Index of types
A
abdbackrule_f
[
Sigs.ABDRULE
]
abdgenrule_f
[
Sigs.ABDRULE
]
abdinfrule_f
[
Sigs.ABDRULE
]
abdrule_t
[
Sigs.ABDUCER
]
abstract1
[
Sl_heap_rho
]
abstract1
[
Sl_heap
]
abstract2
[
Sl_heap_rho
]
abstract2
[
Sl_heap
]
abstract_node
[
Soundcheck
]
Abstract proof node type.
axiom_f
[
Sigs.PROOFRULE
]
B
backrule_f
[
Sigs.PROOFRULE
]
C
continuation
[
Sl_unify.S
]
The type of continuations accepted by SL cps-unifiers
continuation
[
Unification
]
The type of continuations accepted by CPS-unifiers
cps_backtracker
[
Unification
]
cps_unifier
[
Unification
]
The type of continuation-passing-style unifiers that may accept an initial solution state.
D
defs_t
[
Sigs.ABDUCER
]
defs_t
[
Sigs.ABDRULE
]
E
elt
[
Tagpairs
]
elt
[
Hashset.S
]
I
infrule_app
[
Sigs.ABDRULE
]
infrule_app
[
Sigs.PROOFRULE
]
infrule_f
[
Sigs.PROOFRULE
]
N
node_t
[
Sigs.PROOF
]
P
predicate
[
Fun
]
proof_t
[
Sigs.ABDUCER
]
proof_t
[
Sigs.ABDRULE
]
proof_t
[
Sigs.PROOFRULE
]
R
realizer
[
Unification
]
rule_t
[
Sigs.PROVER
]
rule_t
[
Sigs.ABDRULE
]
ruleapp_t
[
Sigs.SEQTACTICS
]
S
select_f
[
Sigs.ABDRULE
]
select_f
[
Sigs.PROOFRULE
]
seq_t
[
Sigs.ABDRULE
]
seq_t
[
Sigs.PROOFRULE
]
seq_t
[
Sigs.SEQTACTICS
]
seq_t
[
Sigs.PROOF
]
seq_t
[
Sigs.NODE
]
Sequent type used for building proof nodes.
state
[
Sl_unify.S
]
State maintained by unifiers.
state_check
[
Sl_unify.S
]
Predicates that check unifier states for validity
state_update
[
Unification
]
symheap
[
Sl_heap_rho
]
symheap
[
Sl_heap
]
T
t
[
Tl_form_ltl.Form
]
t
[
Tl_form.Form
]
t
[
VarManager.SubstSig
]
Abstract type of substitutions
t
[
Int
]
t
[
Strng
]
t
[
Utilsigs.OrderedContainer
]
t
[
Utilsigs.BasicType
]
t
[
Soundcheck
]
The type of abstracted proof as a map from ints to nodes.
t
[
Sigs.ABDRULE
]
t
[
Sigs.PROOFRULE
]
The type of proof rules: Proof rules are functions that take an open node in a proof (i.e.
t
[
Sigs.SEQTACTICS
]
t
[
Sigs.PROOF
]
Proof type.
t
[
Sigs.NODE
]
t
[
Sigs.DEFS
]
t
[
Sigs.SEQUENT
]
t
[
Hashset.HashedType
]
The type of the elements.
t
[
Hashset.S
]
t
[
Blist
]
The type of a t.
U
unifier
[
Sl_unify.S
]
The type of SL unifiers - these always act on pairs of term substitutions and tagpair sets, and only accept continuations that are maps on such pairs.
update_check
[
Sl_unify.S
]
V
var
[
VarManager.SubstSig
]
Abstract type of variables substituted
var
[
VarManager.I
]
var_container
[
VarManager.SubstSig
]
abstract type of containers of variables
var_container
[
VarManager.I
]
varname_class
[
VarManager
]