package libzipperposition

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

Module Ctx.MakeSource

Create a new context

Parameters

module X : PARAMETERS

Signature

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

current ordering on terms

Sourceval selection_fun : unit -> Selection.t

selection function for clauses

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

Current signature

Utils

Compare two terms

Sourceval select : Selection.t
Sourceval eta_normalize : Logtk.Term.t -> Logtk.Term.t

eta_normalize a term (expand or reduce or neutral, depending on cli options)

Sourceval lost_completeness : unit -> unit

To be called when completeness is not preserved

Sourceval is_completeness_preserved : unit -> bool

Check whether completeness was preserved so far

Sourceval add_signature : Logtk.Signature.t -> unit

Merge the given signature with the context's one

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

Find the type of the given symbol

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

Unsafe version of find_signature.

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

Declare the type of a symbol (updates signature)

Sourceval on_signature_update : Logtk.Signature.t Logtk.Signal.t
Sourceval set_injective_for_arg : Logtk.ID.t -> int -> unit
Sourceval is_injective_for_arg : Logtk.ID.t -> int -> bool

Literals

Sourcemodule Lit : sig ... end