eqtype term
STRUCTURE
Term
SYNOPSIS
ML datatype of HOL terms.
DESCRIPTION
The ML abstract type term represents the set of HOL terms, which is essentially the simply typed lambda calculus of Church. A term may be a variable, a constant, an application of one term to another, or a lambda abstraction.
COMMENTS
Since term is an ML eqtype, any two terms tm1 and tm2 can be tested for equality by tm1 = tm2. However, the fundamental notion of equality for terms is implemented by aconv.

Since term is an abstract type, access to its representation is mediated by the interface presented by the Term structure.

SEEALSO
hol_type
HOL  Kananaskis-14