package logtk

You can search for identifiers within the package.

in-package search v0.2.0

package logtk

logtk
- Logtk
- LogtkCache
  - Dummy
    
    X
  - Dummy2
    
    X
    
    Y
  - EQ
  - HASH
  - LRU
    
    X
  - Linear
    
    X
  - Linear2
    
    X
    
    Y
  - Replacing
    
    X
  - Replacing2
    
    X
    
    Y
  - S
  - S2
- LogtkCnf
- LogtkComparison
  - PARTIAL_ORD
- LogtkCongruence
  - FO
  - HO
  - Make
    
    T
  - S
  - TERM
- LogtkDBEnv
- LogtkDtree
  - Default
  - Make
    
    E
- LogtkFOTerm
  - AC
    
    A
  - AC_SPEC
  - Classic
  - Pos
  - Seq
  - T2LogtkCache
  - TLogtkCache
  - TPTP
    
    Arith
  - Tbl
- LogtkFastFingerprint
  - Make
    
    Leaf
- LogtkFeatureVector
  - Make
    
    C
    
    Feature
- LogtkFingerprint
  - Make
    
    Leaf
- LogtkFormula
  - FO
    
    Base
    
    Seq
    
    TPTP
  - Make
    
    Base
    
    MyT
    
    Seq
    
    TPTP
    
    Seq
    
    TPTP
  - Map
    
    From
    
    Base
    
    Seq
    
    TPTP
    
    To
    
    Base
    
    Seq
    
    TPTP
  - S
    
    Base
    
    Seq
    
    TPTP
  - TERM
    
    Seq
    
    TPTP
- LogtkFormulaShape
- LogtkHORewriting
  - Seq
- LogtkHOTerm
  - LogtkCache
  - Pos
  - Seq
  - TPTP
  - Tbl
  - any_visitor
  - id_visitor
- LogtkHashcons
  - HashedLogtkType
  - Make
    
    X
  - S
- LogtkIArray
  - Seq
- LogtkIndex
  - BasicEquation
  - CLAUSE
  - EQUATION
  - LEAF
  - MakeLeaf
  - SUBSUMPTION_IDX
    
    C
  - TERM_IDX
    
    Leaf
  - UNIT_IDX
    
    E
- LogtkInterfaces
  - EQ
  - GROUP
  - HASH
  - ITER
  - MONOID
  - ORD
  - PRINT
  - PRINT1
  - PRINT_DE_BRUIJN
  - PRINT_OVERLOAD
- LogtkLambda
- LogtkLazyGraph
  - Dot
  - Full
  - Heap
  - Infix
  - Mutable
- LogtkLazyList
- LogtkMultiset
  - Make
    
    Seq
  - S
    
    Seq
- LogtkNPDtree
  - Make
    
    E
  - MakeTerm
    
    Leaf
- LogtkOptions
- LogtkOrdering
  - Default
  - Make
    
    P
    
    Constr
    
    Seq
- LogtkOrdering_intf
  - S
    
    Prec
    
    Constr
    
    Seq
- LogtkParseLocation
- LogtkPartialOrder
  - ELEMENT
  - Make
    
    E
- LogtkPartialOrder_intf
  - S
- LogtkPosition
  - Build
- LogtkPrecedence
  - Constr
  - Default
    
    Constr
    
    Seq
  - Make
    
    Constr
    
    Seq
    
    Sym
  - SYMBOL
  - Seq
- LogtkPrecedence_intf
  - S
    
    Constr
    
    Seq
- LogtkPrologTerm
  - Seq
  - TPTP
  - id_visitor
  - visitor
- LogtkRewriting
  - FormRW
  - MakeOrdered
    
    E
  - MakeTRS
    
    I
    
    E
  - ORDERED
    
    E
  - SIG_TRS
  - TRS
- LogtkScopedTerm
  - DB
  - Kind
  - Pos
  - Seq
  - Tbl
- LogtkSignature
  - Seq
  - TPTP
    
    Arith
- LogtkSkolem
- LogtkSourced
- LogtkSubsts
  - FO
  - Form
  - HO
  - Renaming
  - SPECIALIZED
  - Ty
- LogtkSymbol
  - ArithOp
  - Base
  - Seq
  - TPTP
    
    Arith
- LogtkTransform
  - DAG
    
    Form
  - FORM
  - FormDag
    
    Form
  - MakeDAG
    
    Form
- LogtkType
  - Conv
  - Seq
  - TPTP
- LogtkTypeInference
  - Closure
  - Ctx
  - FO
  - HO
  - S
- LogtkTypedPrologTerm
  - Seq
  - Subst
  - Visitor
- LogtkUnif
  - FO
  - Form
  - HO
  - NARY
  - Nary
  - Ty
  - UNARY
  - Unary
- LogtkUtil
  - Exn
  - Flag
  - Section

Legend:
Library
Module
Module type
Parameter
Class
Class type

type t

type elt = elt

val empty : t

val add : t -> LogtkIndex.term -> elt -> t

val remove : t -> LogtkIndex.term -> elt -> t

val is_empty : t -> bool

val iter : t -> (LogtkIndex.term -> elt -> unit) -> unit

val fold : t -> 'a -> ('a -> LogtkIndex.term -> elt -> 'a) -> 'a

val size : t -> int

val fold_unify : 
  ?subst:LogtkIndex.subst ->
  t ->
  LogtkIndex.scope ->
  LogtkIndex.term ->
  LogtkIndex.scope ->
  'a ->
  ('a -> LogtkIndex.term -> elt -> LogtkIndex.subst -> 'a) ->
  'a

LogtkUnify the given term with indexed terms

val fold_match : 
  ?allow_open:bool ->
  ?subst:LogtkIndex.subst ->
  t ->
  LogtkIndex.scope ->
  LogtkIndex.term ->
  LogtkIndex.scope ->
  'a ->
  ('a -> LogtkIndex.term -> elt -> LogtkIndex.subst -> 'a) ->
  'a

Match the indexed terms against the given query term

val fold_matched : 
  ?allow_open:bool ->
  ?subst:LogtkIndex.subst ->
  t ->
  LogtkIndex.scope ->
  LogtkIndex.term ->
  LogtkIndex.scope ->
  'a ->
  ('a -> LogtkIndex.term -> elt -> LogtkIndex.subst -> 'a) ->
  'a

Match the query term against the indexed terms