@spec add_subst([HOL.Data.substitution()], HOL.Data.substitution(), [atom()]) :: [
  HOL.Data.substitution()
]

Adds a single substitution to a list of substitutions. The new substitution is applied to all terms in the other substitutions, keeping the list idempotent.

Substitutions using unique free variables with a tag that is in fvar_tags_not_add are not added to the list, but still apply their substitution to the terms.

Example

iex> x = mk_free_var("x", mk_type(:i))
iex> y = mk_free_var("y", mk_type(:i))
iex> subst_list = [mk_substitution(y, mk_term(x))]
iex> new_subst = mk_substitution(x, mk_const_term("c", mk_type(:i)))
iex> add_subst(subst_list, new_subst) |> PrettyPrint.pp_subst()
"x <- c | y <- c"

@spec subst(
  [HOL.Data.substitution()] | HOL.Data.substitution(),
  HOL.Data.hol_term()
) :: HOL.Data.hol_term()

Applies a singular substitution or a list of substitutions to a term

Example

# Create Term
iex> x = mk_free_var("x", mk_type(:i, [mk_type(:i)]))
iex> term = mk_term(x) |> mk_appl_term(mk_const_term("c", mk_type(:i)))
iex> PrettyPrint.pp_term(term)
"(x c)"
# Create substitution
iex> term_y = mk_free_var_term("y", mk_type(:i, [mk_type(:i)]))
iex> substitution = mk_substitution(x, term_y)
iex> subst(substitution, term) |> PrettyPrint.pp_term()
"(y c)"