inst : (hol_type * hol_type) list -> term -> term

SYNOPSIS
Instantiate type variables in a term.

DESCRIPTION
The call inst [ty1,tv1; ...; tyn,tvn] t will systematically replace each type variable tvi by the corresponding type tyi inside the term t. Bound variables will be renamed if necessary to avoid capture.

FAILURE CONDITIONS
Never fails. Repeated type variables in the instantiation list are not detected, and the first such element will be used.

EXAMPLE
Here is a simple example:
  # inst [`:num`,`:A`] `x:A = x`;;
  val it : term = `x = x`

  # type_of(rand it);;
  val it : hol_type = `:num`
To construct an example where variable renaming is necessary we need to construct terms with identically-named variables of different types, which cannot be done directly in the term parser:
  # let tm = mk_abs(`x:A`,`x + 1`);;
  val tm : term = `\x. x + 1`
Note that the two variables x are different; this is a constant boolean function returning x + 1. Now if we instantiate type variable :A to :num, we still get a constant function, thanks to variable renaming:
  # inst [`:num`,`:A`] tm;;
  val it : term = `\x'. x + 1`
It would have been incorrect to just keep the same name, for that would have been the successor function, something different.

SEE ALSO
subst, type_subst, vsubst.