- SYNOPSIS
-
The type variable `:A`.
- DESCRIPTION
-
This name is bound to the HOL type :A.
- FAILURE CONDITIONS
-
Not applicable.
- USES
-
Exploiting the very common type variable :A inside derived rules (e.g. an
instantiation list for inst or type_subst) without the inefficiency or
inconvenience of calling a quotation parser or explicit constructor.
- SEE ALSO
-
bty, bool_ty.