package logtk

  1. Overview
  2. Docs
package logtk
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module NPDtree.MakeTermSource

Parameters

Signature

Sourcetype t
Sourcetype elt = X.t
Sourcemodule Leaf : Index_intf.LEAF with type elt = elt
Sourceval name : string
Sourceval empty : unit -> t
Sourceval is_empty : t -> bool
Sourceval size : t -> int
Sourceval add : t -> Index_intf.term -> elt -> t
Sourceval add_seq : t -> (Index_intf.term * elt) Iter.t -> t
Sourceval add_list : t -> (Index_intf.term * elt) list -> t
Sourceval remove : t -> Index_intf.term -> elt -> t
Sourceval remove_seq : t -> (Index_intf.term * elt) Iter.t -> t
Sourceval remove_list : t -> (Index_intf.term * elt) list -> t
Sourceval iter : t -> (Index_intf.term -> elt -> unit) -> unit
Sourceval fold : t -> ('a -> Index_intf.term -> elt -> 'a) -> 'a -> 'a

Retrieves a decidable fragment of unifiables. Only one unifier per subterm.

Sourceval retrieve_unifiables_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.t

Retrieves all unifiables. The set of unifiers is potentially infinite. Because HO unification is undecidable, the sequence is intersperced with `None`s to ensure termination for each element of the sequence.

print oneself in DOT into the given file