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
|
\DOC term_of_preterm
\TYPE {term_of_preterm : preterm -> term}
\SYNOPSIS
Converts a preterm into a term.
\DESCRIBE
HOL Light uses ``pretypes'' and ``preterms'' as intermediate structures for
parsing and typechecking, which are later converted to types and terms. A call
{term_of_preterm ptm} attempts to convert preterm {ptm} into a HOL term.
\FAILURE
Fails if some constants used in the preterm have not been defined, or if there
are other inconsistencies in the types so that a consistent typing cannot be
arrived at.
\COMMENTS
Only users seeking to change HOL's parser and typechecker quite radically need
to use this function.
\SEEALSO
preterm_of_term, retypecheck, type_of_pretype.
\ENDDOC
|
