package logtk
Module Make.Leaf
type elt = eltval empty : tval add : t -> Index_intf.term -> elt -> tval remove : t -> Index_intf.term -> elt -> tval update_leaf : t -> Index_intf.term -> (elt -> bool) -> tval is_empty : t -> boolval iter : t -> (Index_intf.term -> elt -> unit) -> unitval fold : t -> 'a -> ('a -> Index_intf.term -> elt -> 'a) -> 'aval size : t -> intval fold_unify :
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Unif_subst.t) Iter.tval fold_unify_complete :
unif_alg:(Term.t Scoped.t -> Term.t Scoped.t -> Unif_subst.t option OSeq.t) ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Unif_subst.t option OSeq.t) Iter.tval fold_match :
?subst:Index_intf.subst ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Index_intf.subst) Iter.tMatch the indexed terms against the given query term
val fold_matched :
?subst:Index_intf.subst ->
t Scoped.t ->
Index_intf.term Scoped.t ->
(Index_intf.term * elt * Index_intf.subst) Iter.tMatch the query term against the indexed terms