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 retypecheck
\TYPE {retypecheck : (string * pretype) list -> preterm -> preterm}
\SYNOPSIS
Typecheck a term, iterating over possible overload resolutions.
\DESCRIBE
This is the main HOL Light typechecking function. Given an environment {env} of
pretype assignments for variables, it assigns a pretype to all variables and
constants, including performing resolution of overloaded constants based on
what type information there is. Normally, this happens implicitly when a term
is entered in the quotation parser.
\FAILURE
Fails if some terms cannot be consistently assigned a type.
\COMMENTS
Only users seeking to change HOL's parser and typechecker quite radically need
to use this function.
\SEEALSO
term_of_preterm.
\ENDDOC
|
