HOL: Reference

hol_type

Type.eqtype hol_type

Type of HOL types.

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.

See also

Term.term