package term-tools

  1. Overview
  2. Docs

Module Make.SubstSource

Handling substitutions.

Sourcetype term = Term.t

The type of terms

type var := int
Sourcetype t

The type of substitutions

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

empty () is the empty substitution.

Sourceval is_empty : t -> bool

is_empty subst checks whether equal subst empty

Sourceval equal : t -> t -> bool

equal s1 s2 checks equality of substitutions.

Sourceval 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.

Sourceval 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

Sourceval unsafe_add : var -> term -> t -> t

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

Sourceval 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.

Sourceval 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