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
|
\DOC mk_const
\TYPE {mk_const : string * (hol_type * hol_type) list -> term}
\SYNOPSIS
Produce constant term by applying an instantiation to its generic type.
\DESCRIBE
This is the basic way of constructing a constant term in HOL Light, applying a
specific instantiation (by {type_subst}) to its generic type. It may sometimes
be more convenient to use {mk_mconst}, which just takes the desired type for
the constant and finds the instantiation itself; that is also a natural inverse
for {dest_const}. However, {mk_const} is likely to be significantly faster.
\FAILURE
Fails if there is no constant of the given type.
\EXAMPLE
{
# get_const_type "=";;
val it : hol_type = `:A->A->bool`
# mk_const("=",[`:num`,`:A`]);;
val it : term = `(=)`
# type_of it;;
val it : hol_type = `:num->num->bool`
# mk_const("=",[`:num`,`:A`]) = mk_mconst("=",`:num->num->bool`);;
val it : bool = true
}
\SEEALSO
dest_const, is_const, mk_mconst, type_subst.
\ENDDOC
|
