package libzipperposition

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

Create a new context

Parameters

module X : PARAMETERS

Signature

val sk_ctx : unit -> Logtk.Skolem.ctx
val ord : unit -> Logtk.Ordering.t

current ordering on terms

val selection_fun : unit -> Selection.t

selection function for clauses

val set_selection_fun : Selection.t -> unit
val set_ord : Logtk.Ordering.t -> unit
val signature : unit -> Logtk.Signature.t

Current signature

val renaming : Logtk.Subst.Renaming.t

Utils

Compare two terms

val select : Selection.t
val bool_select : Bool_selection.t
val lost_completeness : unit -> unit

To be called when completeness is not preserved

val is_completeness_preserved : unit -> bool

Check whether completeness was preserved so far

val add_signature : Logtk.Signature.t -> unit

Merge the given signature with the context's one

val find_signature : Logtk.ID.t -> Logtk.Type.t option

Find the type of the given symbol

val find_signature_exn : Logtk.ID.t -> Logtk.Type.t

Unsafe version of find_signature.

val declare : Logtk.ID.t -> Logtk.Type.t -> unit

Declare the type of a symbol (updates signature)

val declare_syms : (Logtk.ID.t * Logtk.Type.t) list -> unit

Declare multiple symbols (more efficient that calling declare function incrementally)

val on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
val on_signature_update : Logtk.Signature.t Logtk.Signal.t
val set_injective_for_arg : Logtk.ID.t -> int -> unit
val is_injective_for_arg : Logtk.ID.t -> int -> bool

Literals

module Lit : sig ... end
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