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