retypecheck : (string * pretype) list -> preterm -> preterm
- SYNOPSIS
-
Typecheck a term, iterating over possible overload resolutions.
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
term_of_preterm.