package libzipperposition

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

Module Make.TermIndexSource

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

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

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct