package term-tools

  1. Overview
  2. Docs

Parameters

module P : Intf.Signature
module M : Intf.Map with type key = int
module T : Intf.Term_core with type prim = P.t

Signature

type term = T.t

The type of terms

type var := int
type t

The type of substitutions

val of_seq : (var * term) Seq.t -> t
val to_seq : t -> (var * term) Seq.t
val to_seq_keys : t -> var Seq.t
val pp : Format.formatter -> t -> unit
val empty : unit -> t

empty () is the empty substitution.

val is_empty : t -> bool

is_empty subst checks whether equal subst empty

val equal : t -> t -> bool

equal s1 s2 checks equality of substitutions.

val get : var -> t -> term option

get k state returns Some v if the key k is associated to the value v in state, or None otherwise.

val add : var -> term -> t -> t

add v t subst adds a mapping from v to t in subst. If v is already in the domain of subst, the previous mapping is replaced.

Raises Invalid_argument if t is a variable equal to v

val unsafe_add : var -> term -> t -> t

unsafe_add does as add but doen't check for validity of the mapping.

val lift : t -> term -> term

lift subst term applies the substitution subst to term. Note that lift does not perform an occur check: do not use with substitutions that are not well-founded.

val union : t -> t -> t

union s1 s2 computes the union of s1 and s2.

Raises Invalid_argument if s1 and s2 have overlapping domains.

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