package inferno

  1. Overview
  2. Docs
module Make (S : sig ... end) : sig ... end

This module implements a unification algorithm for first-order terms whose structure is specified by the parameter S. In particular, the operation S.conjunction specifies how two structural constraints bearing on a variable are combined.