1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
\DOC type_of_pretype
\TYPE {type_of_pretype : pretype -> hol_type}
\SYNOPSIS
Converts a pretype to a type.
\DESCRIBE
HOL Light uses ``pretypes'' and ``preterms'' as intermediate structures for
parsing and typechecking, which are later converted to types and terms. A call
{type_of_pretype pty} attempts to convert pretype {pty} into a HOL type.
\FAILURE
Fails if some type constants used in the pretype have not been defined, or if
the arities are wrong.
\COMMENTS
Only users seeking to change HOL's parser and typechecker quite radically need
to use this function.
\SEEALSO
pretype_of_type, retypecheck, term_of_preterm.
\ENDDOC
|
