This is the datatype for internal HOL terms. It has 4 classes, corresponding to the 4 primitive syntactic categories of term:

 

Variable - This denotes an occurrence of a variable. It has name and type attributes. Any two occurrences of variables within a given object refer the same entity iff they have the same name, type and scope.

 

Constant - This denotes an occurrence of a constant. It has name and type attributes, where the name must be a declared constant's name and the type must match the declared constant's generic type.

 

Function Application - This consists of a function subterm and an argument subterm, where the function's type must be a function type with domain type equal to the argument's type.

 

Lambda Astraction - This consists of a binding variable and a body subterm. It bounds the scope of the binding variable to the body, and this is the only primitive means of bounding variable scope.