Index of types


A
arith_view [LogtkSymbol.ArithOp]
arity_result [LogtkType]
attribute [LogtkLazyGraph.Dot]
Dot attribute

C
clause [LogtkCnf]
Basic clause representation, as list of literals
combination [LogtkComparison]
Lexicographic combination of comparators.
comparator [LogtkComparison]
comparison [LogtkComparison]
connective [LogtkSymbol]
const_symbol [LogtkSymbol]
ctx [LogtkSkolem]
Context needed to create new symbols
ctx [LogtkType.Conv]

D
default_types [LogtkTypeInference]
definition [LogtkSkolem]

E
edge_type [LogtkLazyGraph.Full]
elt [LogtkPartialOrder_intf.S]
Elements that can be compared
elt [LogtkMultiset.S]
Elements of the multiset
elt [LogtkHashcons.S]
LogtkHashconsed objects
elt [LogtkIndex.TERM_IDX]
elt [LogtkIndex.LEAF]
env [LogtkUnif]
env [LogtkScopedTerm.DB]

F
feature_vector [LogtkFeatureVector.Make]
a vector of feature
fingerprint_fun [LogtkFastFingerprint]
fingerprint_fun [LogtkFingerprint]
flag [LogtkScopedTerm]
form [LogtkTransform]
form [LogtkFormulaShape]
form [LogtkRewriting.FormRW]
form [LogtkCnf]
form [LogtkFormula.S]
func [LogtkCache.S2]

G
gen [LogtkUtil.Flag]
Generator of flags
graph [LogtkLazyGraph]

K
key [LogtkCache.S]
key1 [LogtkCache.S2]
key2 [LogtkCache.S2]

L
lits [LogtkIndex]
Sequence of literals, as a cheap abstraction on query clauses
location [LogtkTypedPrologTerm]
location [LogtkPrologTerm]

M
monad [LogtkTypeInference.Closure]
monad used for traversal

N
nat [LogtkScopedTerm]
node [LogtkLazyGraph]
node [LogtkLazyList]

O
options [LogtkCnf]
or_error [LogtkTypedPrologTerm]
or_error [LogtkTypeInference]
or_error [LogtkUtil]
ordering [LogtkOrdering_intf.S]

P
path [LogtkLazyGraph]
A reverse path (from the last element of the path to the first).
polarity [LogtkSkolem]
position [LogtkPosition]
precedence [LogtkPrecedence_intf.S]
print_hook [LogtkInterfaces.PRINT_DE_BRUIJN]
User-provided hook that can be used to print terms (for composite cases) before the default printing occurs.
profiler [LogtkUtil]

R
res [LogtkUnif]
result [LogtkUnif.NARY]
rhs [LogtkIndex.UNIT_IDX]
Right hand side of equation
rhs [LogtkIndex.EQUATION]
An equation can have something other than a term as a right-hand side, for instance a formula.
rule [LogtkRewriting.FormRW]
rewrite rule, from left to right
rule [LogtkRewriting.SIG_TRS]
rewrite rule, from left to right
rule [LogtkHORewriting]

S
scope [LogtkLambda]
scope [LogtkIndex]
scope [LogtkUnif]
scope [LogtkSubsts]
A scope is an integer.
scoped [LogtkSubsts]
sequence [LogtkUnif]
stat [LogtkUtil]
subst [LogtkIndex]
subst [LogtkUnif]
subst [LogtkSubsts]
symbol [LogtkCnf]
symbol [LogtkOrdering_intf.S]
symbol [LogtkPrecedence_intf.S]
symbol [LogtkFormula]
symbol [LogtkHOTerm]
symbol [LogtkType]
symbol [LogtkFOTerm]
symbol [LogtkScopedTerm]
symbol_status [LogtkPrecedence_intf]
symbol_status [LogtkPrecedence]

T
t [LogtkLazyGraph.Heap]
t [LogtkLazyGraph.Mutable]
Mutable graph
t [LogtkLazyGraph]
Lazy graph structure.
t [LogtkIArray]
Array of values of type 'a
t [LogtkLazyList]
t [LogtkPartialOrder.ELEMENT]
t [LogtkPartialOrder_intf.S]
the partial order on elements of type elt
t [LogtkMultiset.S]
A multiset of elements of type 'a
t [LogtkParseLocation]
t [LogtkCache.EQ]
t [LogtkHashcons.HashedLogtkType]
t [LogtkHashcons.S]
LogtkHashconsing table
t [LogtkTypedPrologTerm.Subst]
t [LogtkTypedPrologTerm.Visitor]
Fold-like operation that maps a term into a value of type 'a
t [LogtkTypedPrologTerm]
t [LogtkSourced]
t [LogtkTransform.FORM]
t [LogtkTransform.DAG]
t [LogtkTransform]
t [LogtkRewriting.FormRW]
t [LogtkRewriting.SIG_TRS]
t [LogtkRewriting.ORDERED]
t [LogtkFeatureVector.Make.Feature]
a function that computes a given feature on clauses
t [LogtkCongruence.TERM]
t [LogtkCongruence.S]
Represents a congruence
t [LogtkIndex.UNIT_IDX]
t [LogtkIndex.SUBSUMPTION_IDX]
t [LogtkIndex.CLAUSE]
t [LogtkIndex.TERM_IDX]
t [LogtkIndex.EQUATION]
t [LogtkIndex.LEAF]
t [LogtkHORewriting]
rewrite system
t [LogtkOrdering_intf.S]
Partial ordering on terms
t [LogtkPrecedence.SYMBOL]
t [LogtkPrecedence_intf.S.Constr]
A partial order on symbols, used to make the precedence more precise
t [LogtkPrecedence_intf.S]
Total LogtkOrdering on a finite number of symbols, plus a few more data (weight for KBO, status for RPC)
t [LogtkComparison.PARTIAL_ORD]
t [LogtkComparison]
t [LogtkOptions]
Options that can be set by the user
t [LogtkTypeInference.Closure]
t [LogtkTypeInference.Ctx]
t [LogtkSignature]
A signature maps symbols to types
t [LogtkSubsts.SPECIALIZED]
t [LogtkSubsts.Renaming]
t [LogtkSubsts]
A substitution that binds term variables to other terms
t [LogtkFormula.TERM]
t [LogtkFormula.S]
t [LogtkHOTerm]
t [LogtkPosition.Build]
t [LogtkPosition]
A position is a path in a tree
t [LogtkDBEnv]
An environment that maps De Bruijn indices to values of type 'a.
t [LogtkInterfaces.MONOID]
t [LogtkInterfaces.ITER]
t [LogtkInterfaces.PRINT_DE_BRUIJN]
t [LogtkInterfaces.PRINT_OVERLOAD]
t [LogtkInterfaces.PRINT1]
t [LogtkInterfaces.PRINT]
t [LogtkInterfaces.ORD]
t [LogtkInterfaces.EQ]
t [LogtkPrologTerm]
t [LogtkUtil.Section]
t [LogtkType]
LogtkType is a subtype of the general structure LogtkScopedTerm.t, with explicit conversion
t [LogtkCache.S2]
t [LogtkCache.S]
t [LogtkFOTerm]
t [LogtkScopedTerm.Kind]
"kind" of a term, i.e.
t [LogtkScopedTerm]
Abstract type of term
t [LogtkSymbol]
term [LogtkTypedPrologTerm]
term [LogtkLambda]
term [LogtkTransform]
term [LogtkFormulaShape]
term [LogtkCongruence.S]
term [LogtkIndex]
term [LogtkHORewriting]
term [LogtkOrdering_intf.S]
term [LogtkUnif.UNARY]
term [LogtkUnif.NARY]
term [LogtkSubsts.SPECIALIZED]
term [LogtkSubsts]
term [LogtkFormula.S]
term [LogtkHOTerm]
term [LogtkInterfaces.PRINT_DE_BRUIJN]
term [LogtkPrologTerm]
term [LogtkFOTerm]
term [LogtkScopedTerm]
term_set [LogtkFormula.S]
transformation [LogtkTransform]
traverse_event [LogtkLazyGraph.Full]
ty [LogtkType]
type_ [LogtkFormula]
type_result [LogtkScopedTerm]
typed [LogtkTypeInference.S]
typed term
typed_form [LogtkTypeInference.FO]

U
untyped [LogtkTypeInference.S]
untyped term

V
view [LogtkTypedPrologTerm]
view [LogtkFormula.S]
view [LogtkHOTerm]
view [LogtkPrologTerm]
view [LogtkType]
view [LogtkFOTerm.Classic]
view [LogtkFOTerm]
view [LogtkScopedTerm]

W
weight_fun [LogtkPrecedence_intf.S]