gen_tyvar_sigma
boolSyntax.gen_tyvar_sigma : hol_type list -> (hol_type,hol_type) Lib.subst
Generates an instantiation mapping each type to a fresh type variable
A call to gen_tyvar_sigma tys generates an instantiation (a list of
{redex,residue} pairs) mapping the types in tys to fresh type
variables (generated in turn with gen_tyvar). Standard practice would
be to have tys be a list of distinct type variables, but this is not
checked.
Failure
Never fails.
Example
> gen_tyvar_sigma [“:'c”, “:'a”, “:'bob”];
val it =
[{redex = “:γ”, residue = “:%%gen_tyvar%%32”},
{redex = “:α”, residue = “:%%gen_tyvar%%33”},
{redex = “:'bob”, residue = “:%%gen_tyvar%%34”}]:
(hol_type, hol_type) Lib.subst