Index (u.49a4c3110aa1418b07193ba107865015.logtk.2.0.doc.logtk.Logtk.Index)

Generic term indexing

Interfaces for indexing terms (for unification, matching) and clauses (for subsumption)

type term = Term.t

type subst = Subst.t

A leaf maps terms to a set of elements

module type LEAF = Index_intf.LEAF

module MakeLeaf (X : Set.OrderedType) : LEAF with type elt = X.t

module type TERM_IDX = Index_intf.TERM_IDX

module type CLAUSE = Index_intf.CLAUSE

A subsumption index (non perfect!)

module type SUBSUMPTION_IDX = Index_intf.SUBSUMPTION_IDX

module type EQUATION = Index_intf.EQUATION

module BasicEquation : 
  EQUATION with type t = Term.t * Term.t and type rhs = Term.t

module type UNIT_IDX = Index_intf.UNIT_IDX