term_of_preterm : preterm -> term
- SYNOPSIS
-
Converts a preterm into a term.
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
preterm_of_term, retypecheck, type_of_pretype.