1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
\DOC tysubst
\TYPE {tysubst : (hol_type * hol_type) list -> hol_type -> hol_type}
\DESCRIBE
The call {tysubst [ty1',ty1; ... ; tyn',tyn] ty} will systematically traverse
the type {ty} and replace the topmost instances of any {tyi} encountered with
the corresponding {tyi'}. In the (usual) case where all the {tyi} are type
variables, this is the same as {type_subst}, but also works when they are not.
\FAILURE
Never fails. If several {tyi} are the same, the first one in the list will be
used to determine the substitution.
\EXAMPLE
{
# tysubst [`:num`,`:A`; `:bool`,`:B`] `:A->(B)list->A#B#C`;;
val it : hol_type = `:num->(bool)list->num#bool#C`
# tysubst [`:A`,`:(num)list`] `:num->(num)list->(num)list`;;
val it : hol_type = `:num->A->A`
}
\SEEALSO
inst, tysubst.
\ENDDOC
|
