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 null_inst
\TYPE {null_inst : instantiation}
\SYNOPSIS
Empty instantiation.
\DESCRIBE
Several functions use objects of type {instantiation}, consisting of type and
term instantiations and higher-order matching information. This instantiation
{null_inst} is the trivial instantiation that does nothing.
\FAILURE
Not applicable.
\EXAMPLE
Instantiating a term with it has no effect:
{
# instantiate null_inst `x + 1 = 2`;;
val it : term = `x + 1 = 2`
}
\SEEALSO
instantiate, INSTANTIATE, INSTANTIATE_ALL, term_match.
\ENDDOC
|
