module Subst:sig..end
Substitutions (or environments)
The module Matcher.Subst contains infrastructure to deal with
substitutions, i.e., functions from variables to terms. Only a
restricted subsets of these functions need to be exported.
As expected, a particular substitution can be used to instantiate a pattern.
type
val sprint : t -> string
val instantiate : t -> Matcher.Terms.t -> Matcher.Terms.t
val to_list : t -> (Matcher.var * Matcher.Terms.t) list