package logtk

Variable is bound?

Apply the substitution to the given term/type.

• parameter renaming

  used to desambiguate free variables from distinct scopes

Same as apply, but performs no renaming of free variables. Caution, can entail collisions between scopes!

Add v -> t to the substitution. Both terms have a context.

• raises Invalid_argument

  if v is already bound in the same context, to another term.