Module Make.SubstSource

Sourcetype t = sigma
Sourceval create : ?pool:pool -> unit -> t
Sourceval copy : sigma -> sigma
Sourceval fresh : t -> tau -> var
Sourceval find : t -> term -> term
Sourceval filter : t -> term -> bool
Sourceval add : t -> term -> term -> unit

Must bind lc-closed terms, or raise Invalid_argument

Sourceval add_fun : t -> (term -> term) -> unit

Must bind lc-closed terms, or raise Invalid_argument

Sourceval add_filter : t -> (term -> bool) -> unit

Only modifies terms that pass the filter.

Sourceval add_var : t -> var -> unit

To the pool

Sourceval add_vars : t -> Vars.t -> unit

To the pool

Sourceval add_term : t -> term -> unit

To the pool