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 pretype_of_type
\TYPE {pretype_of_type : hol_type -> pretype}
\SYNOPSIS
Converts a type into a pretype.
\DESCRIBE
HOL Light uses ``pretypes'' and ``preterms'' as intermediate structures for
parsing and typechecking, which are later converted to types and terms. A call
{preterm_of_term `tm`} converts in the other direction, from a normal HOL term
back to a preterm.
\FAILURE
Never fails.
\USES
User manipulation of pretypes is not usually necessary, unless you seek to
radically change aspects of parsing and typechecking.
\SEEALSO
preterm_of_term, type_of_pretype.
\ENDDOC
|
