ty_antiq

Parse.ty_antiq : hol_type -> term

Make a variable named ty_antiq.

Given a type ty, the ML invocation ty_antiq ty returns the HOL variable ty_antiq : ty. This provides a way to antiquote types into terms, which is necessary because the HOL term parser only allows terms to be antiquoted. The use of ty_antiq promotes a type to a term variable which can be antiquoted. The HOL parser detects occurrences of ty_antiq ty and inserts ty as a constraint.

Example

Suppose we want to constrain a term to have type num list, which is bound to ML value ty. Attempting to antiquote ty directly into the term won’t work:

> val ty = ``:num list``;
val ty = “:num list”: hol_type

> “x : ^ty”;
Exception- Type error in function application.
   Function: Parse.Term : term frag list -> term
   Argument: [QUOTE " (*#loc 1 4*)x : ", ANTIQUOTE ty] :
      hol_type frag list
   Reason:
      Can't unify term (*Created from opaque signature*) with
         hol_type (*Created from opaque signature*)
         (Different type constructors)
Fail "Static Errors" raised

Use of ty_antiq solves the problem:

> ``x : ^(ty_antiq ty)``;
val it = “x”: term

> type_of it;
val it = “:num list”: hol_type

See also

Parse.Term