Module `Logtk.Index`

Generic term indexing

module type LEAF = Index_intf.LEAF

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

module type TERM_IDX = Index_intf.TERM_IDX

module type CLAUSE = Index_intf.CLAUSE

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