package um-abt

You can search for identifiers within the package.

in-package search v0.2.0

An OCaml library implementing unifiable abstract binding trees (UABTs)

Install

Dune Dependency

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

Authors

S

Shon Feder

Maintainers

S

shon.feder@gmail.com

Sources

um-abt-v0.1.7.tbz

sha256=9472873b4f485ff1c169d950488133c79efb4b00b757526bfb14a2f043a0480f

sha512=e3ea3990177778ae109082bea0b952b760b4fc9a243f0321367d2927061e3766c0d99679c5e4b13f89532b22ad4993c34f91b625ec40e07f113b9812521f91f4

doc/um-abt/Abt/Make/Unification/index.html

Module `Make.Unification`Source

Sourcemodule Subst : sig ... end

Sourcetype error = [

| `Unification of Var.t option * t * t
| `Occurs of Var.t * t
| `Cycle of Subst.t

]

Errors returned when unification fails

Sourceval unify : t -> t -> (t * Subst.t, error) Result.t

unify a b is Ok (union, substitution) when a and b can be unified into the term union and substitution is the most general unifier. Otherwise it is Error err), for which, see error

Sourceval (=.=) : t -> t -> (t, error) Result.t

a =.= b is unify a b |> Result.map fst

Sourceval (=?=) : t -> t -> bool

a =?= b is true iff a =.= b is an Ok _ value