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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
\DOC inst
\TYPE {inst : (term list -> (type # type) list -> term -> term)}
\SYNOPSIS
Performs type instantiations in a term, avoiding certain ones.
\DESCRIBE
The function {inst} should be used as follows:
{
inst [tm1;...;tmn] [(t1',t1);...;(tn',tn)] tm
}
\noindent where {tm1...tmn} are variables, {t1...tn,t1'...tn'} types and {tm} a
term to be type-instantiated. This call will instantiate, in parallel, the
types {t1'...tn'} for the types {t1...tn} wherever they appear in {tm}
(possibly nowhere). However, if the name (not necessarily the type) of any
variable being instantiated matches one of the {[tm1...tmn]}, it will be
renamed (by adding primes) prior to the instantiation. This is useful to avoid
obscure problems of free variable capture when type-instantiating theorems.
\FAILURE
Fails if the instantiation list is non-empty and some of the {tm1...tmn} are
not simply variables.
\EXAMPLE
{
#inst [] [(":num",":*")] "(x:*) = (x:*)";;
"x = x" : term
#inst ["x:bool"] [(":num",":*")] "(x:*) = (x:*)";;
"x' = x'" : term
#inst [] [(":num",":bool")] "x:bool";;
"x" : term
#type_of it;;
":num" : type
}
\USES
Performing internal functions connected with type instantiation.
\SEEALSO
inst_check, inst_rename_list, inst_type, INST_TYPE.
\ENDDOC
|
