type_of_pretype : pretype -> hol_type
- SYNOPSIS
-
Converts a pretype to a type.
- DESCRIPTION
-
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 CONDITIONS
-
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.
- SEE ALSO
-
pretype_of_type, retypecheck, term_of_preterm.