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_type
s
ty1
and
ty2
can be tested for equality by
ty1 = ty2
.
SEEALSO
term
HOL
Kananaskis-14