package libzipperposition

  1. Overview
  2. Docs
On This Page
  1. Utils
  2. Literals
Library for Zipperposition

Install 

dune-project
 Dependency

github.com Readme Changelog Edit opam file Versions (4)

Authors

  1. S
    Simon Cruanes

Maintainers

  1. S
    simon.cruanes.2007@m4x.org

Sources

1.5.1.tar.gz
md5=cc320f66f10555c54822da624419e003
sha512=f8d5f7a5ae790bf0388d74261673803cf375f91f92f7b413b70db1ce5841ef55343a208f98727c8551d66f1840ab892f1c0c943a34861d14d79ce469b235a2f2

doc/libzipperposition.calculi/Libzipperposition_calculi/Arith_rat/Make/argument-1-E/Ctx/index.html

Module E.Ctx

val ord : unit -> Logtk.Ordering.t

current ordering on terms

val selection_fun : unit -> Libzipperposition.Selection.t

selection function for clauses

val set_selection_fun : Libzipperposition.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 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 on_new_symbol : (Logtk.ID.t * Logtk.Type.t) Logtk.Signal.t
val on_signature_update : Logtk.Signature.t Logtk.Signal.t

Literals

module Lit : sig ... end