eqtype hol_type
STRUCTURE
Type
SYNOPSIS
Type of HOL types.
DESCRIPTION
The ML type hol_type represents the type of HOL types.
COMMENTS
Since hol_type is an ML eqtype, any two hol_types ty1 and ty2 can be tested for equality by ty1 = ty2.
SEEALSO
term
HOL  Trindemossen-1