HOL API: Types and Terms

hol_prover_client.hhol_prover_client.h is a thin RPC client for HOL Light. Each function in it names an operation the prover carries out in its own process, and hands back an opaque handle to the object the prover created. Constructing a term with mk_combmk_comb is therefore not a local allocation: it is a request the prover type-checks and either accepts or rejects.

Four conventions apply to every declaration on this page and on the three pages that follow.

• Every call records a status. After any call, get_last_status()get_last_status() is HOL_STATUS_OKHOL_STATUS_OK or HOL_STATUS_ERRORHOL_STATUS_ERROR, and get_last_error()get_last_error() returns the message for the latter. Checking the status is the recommended discipline: it is uniform across functions whose results are boolbool, intint or voidvoid, where no distinguished failure value exists.
• Failed calls return an empty_*empty_* sentinel, never NULLNULL. The header declares empty_termempty_term, empty_theoremempty_theorem, empty_typeempty_type, empty_conversionempty_conversion and the matching pair values. Test a result with the generic macro IS_NULLIS_NULL, not against NULLNULL — the object types are structs, not pointers. An empty list is a zero-length vector and a perfectly valid value; a null list pointer is the error indication.
• All returned pointers are garbage-collected. Every cstrcstr, every list and the memory behind every handle is managed by the GC the runtime links in. Nothing returned by this API is freed by the caller, and the const char*const char* from get_last_error()get_last_error() may be invalidated by the next call.
• The header is generated; do not edit it. Its declarations come from the prover’s own interface description, which is why the doc comments read like HOL Light’s reference manual. This page reproduces them verbatim, together with the failure conditions the header states.

The connection is process-wide. hol_prover_init()hol_prover_init() establishes it; hol_prover_shutdown()hol_prover_shutdown() tears it down and resets the status, after which hol_prover_init()hol_prover_init() can build a fresh connection in the same process.

hol_status_t get_last_status();

hol_status_t get_last_status();

const char* get_last_error();

const char* get_last_error();

Pointer will probably be invalidated after other calling

void hol_prover_init();

void hol_prover_init();

void hol_prover_shutdown();

void hol_prover_shutdown();

Tears down the current connection (destroys the capnp/kj event loop and socket) and resets status to OK. After this, hol_prover_init() can build a fresh connection in the SAME process. Required so the process can drop its kj event loop before fork() (kj event loops are not fork-safe) and rebuild it afterward. Safe to call when not connected.

The status itself is a plain intint — typedef int hol_status_ttypedef int hol_status_t — with two documented values:

The four object types are opaque structs, each wrapping a pointer the client must not touch:

typedef struct hol_term { void* inner; } hol_term;
typedef struct hol_theorem { void* inner; } hol_theorem;
typedef struct hol_type { void* inner; } hol_type;
typedef struct hol_conversion { void* inner; } hol_conversion;

typedef struct hol_term { void* inner; } hol_term;
typedef struct hol_theorem { void* inner; } hol_theorem;
typedef struct hol_type { void* inner; } hol_type;
typedef struct hol_conversion { void* inner; } hol_conversion;

Because they are structs rather than pointers, a failed call cannot signal failure by returning NULLNULL. It returns a sentinel whose innerinner field is null — empty_termempty_term, empty_theoremempty_theorem, empty_typeempty_type, empty_conversionempty_conversion, and for the paired results empty_term_pairempty_term_pair, empty_thm_pairempty_thm_pair, empty_type_pairempty_type_pair. The header supplies one generic test for all of them:

#define IS_NULL(t)                                      \
  _Generic((t),                                         \
      const char*: __hol_is_null_c_impl_const_char_ptr, \
      char*: __hol_is_null_c_impl_char_ptr,             \
      char: __hol_is_null_c_impl_char,                  \
      hol_term: __hol_is_null_c_impl_hol_term,          \
      hol_theorem: __hol_is_null_c_impl_hol_theorem,    \
      hol_type: __hol_is_null_c_impl_hol_type,          \
      hol_conversion: __hol_is_null_c_impl_hol_conversion)(t)

#define IS_NULL(t)                                      \
  _Generic((t),                                         \
      const char*: __hol_is_null_c_impl_const_char_ptr, \
      char*: __hol_is_null_c_impl_char_ptr,             \
      char: __hol_is_null_c_impl_char,                  \
      hol_term: __hol_is_null_c_impl_hol_term,          \
      hol_theorem: __hol_is_null_c_impl_hol_theorem,    \
      hol_type: __hol_is_null_c_impl_hol_type,          \
      hol_conversion: __hol_is_null_c_impl_hol_conversion)(t)

Check if the term is null

In C this is a _Generic_Generic selection; in C++ the same name is a set of overloads. Both accept a charchar, a char*char*, a const char*const char* and any of the four object types, so IS_NULLIS_NULL is also the right test for a returned string. The remaining test macros cover the aggregate values:

Lists are vectors, not null-terminated arrays. hol_term_listhol_term_list, hol_type_listhol_type_list, hol_theorem_listhol_theorem_list, cstr_listcstr_list, int_listint_list and the pair-list types are all T*T* pointing at vector storage, and the length lives in the vector rather than in a terminator. An empty list is a legitimate value, built with empty_listempty_list:

#define empty_list(typ) ((typ*)vector_create())

#define empty_list(typ) ((typ*)vector_create())

A list with zero length is an empty list, which is valid. A null pointer is not a valid list, and is used to indicate an error.

Several destructors return more than one value, and the header declares a small result struct for each — dest_app_type_resultsdest_app_type_results, dest_comb_resultsdest_comb_results, strip_forall_resultsstrip_forall_results, dest_thm_resultsdest_thm_results, and so on. They are plain structs with named fields, and each appears in the declaration of the function that produces it.

A HOL type is either a type variable or a type constructor applied to a list of argument types. Everything else — the function type, the product type, the list type — is a constructor with a fixed name, and the header provides a convenience layer over mk_app_typemk_app_type and dest_app_typedest_app_type for the common ones.

hol_type mk_var_type(const_cstr s);

hol_type mk_var_type(const_cstr s);

Constructs a type variable of the given name.

• raises — Never fails.

cstr dest_var_type(hol_type ty);

cstr dest_var_type(hol_type ty);

Breaks a type variable down to its name.

• raises — Fails if the type is not a type variable.

hol_type mk_app_type(const_cstr s, hol_type_list tys);

hol_type mk_app_type(const_cstr s, hol_type_list tys);

Constructs a type (other than a variable type).

• raises — Fails if the string is not the name of a known type, or if the type is known but the length of the list of argument types is not equal to the arity of the type constructor.

dest_app_type_results dest_app_type(hol_type ty);

dest_app_type_results dest_app_type(hol_type ty);

Breaks apart a type (other than a variable type).

• raises — Fails if the type is a type variable.

The base types have nullary constructors, none of which can fail:

Function types are the workhorse. list_mk_fun_typelist_mk_fun_type and strip_fun_typestrip_fun_type handle the curried form, so a predicate type such as :num->num->bool:num->num->bool can be built and taken apart in a single call.

hol_type mk_fun_type(hol_type ty1, hol_type ty2);

hol_type mk_fun_type(hol_type ty1, hol_type ty2);

Construct a function type.

• raises — Never fails.

hol_type list_mk_fun_type(hol_type_list tys, hol_type ty);

hol_type list_mk_fun_type(hol_type_list tys, hol_type ty);

Constructs a function type with multiple (curried) parameters.

• raises — Never fails.

dest_fun_type_results dest_fun_type(hol_type ty);

dest_fun_type_results dest_fun_type(hol_type ty);

Breaks apart a function type into domain and range.

• raises — Fails if the type is not a function type.

strip_fun_type_results strip_fun_type(hol_type ty);

strip_fun_type_results strip_fun_type(hol_type ty);

Breaks apart a function type into (curried) domains and range.

• raises — Never fails.

Product and list types follow the same construct / iterate / destruct / strip pattern:

hol_type mk_prod_type(hol_type ty1, hol_type ty2);

hol_type mk_prod_type(hol_type ty1, hol_type ty2);

Constructs a product type.

• raises — Never fails.

hol_type list_mk_prod_type(hol_type_list tys);

hol_type list_mk_prod_type(hol_type_list tys);

Constructs a product type with multiple components in a right-associated way.

• raises — Fails if given zero components.

dest_prod_type_results dest_prod_type(hol_type ty);

dest_prod_type_results dest_prod_type(hol_type ty);

Breaks apart a product type into its two components.

• raises — Fails if the type is not a product type.

hol_type_list strip_prod_type(hol_type ty);

hol_type_list strip_prod_type(hol_type ty);

Breaks apart a product type into its multiple components.

• raises — Never fails.

hol_type mk_list_type(hol_type ty);

hol_type mk_list_type(hol_type ty);

Constructs a list type.

• raises — Never fails.

hol_type dest_list_type(hol_type ty);

hol_type dest_list_type(hol_type ty);

Breaks apart a list type into its element type.

• raises — Fails if the type is not a list type.

Each family has a test, and none of the tests fails — a test simply answers falsefalse for a type of another shape:

Finally, the operations that relate types to terms and to one another:

hol_type_list type_tyvars(hol_type ty);

hol_type_list type_tyvars(hol_type ty);

Returns a list of the type variables in a type.

• raises — Never fails.

hol_type type_subst(hol_type_pair_list ty_pairs, hol_type ty);

hol_type type_subst(hol_type_pair_list ty_pairs, hol_type ty);

Substitutes chosen types for type variables in a type.

• raises — Never fails.

hol_type type_of(hol_term tm);

hol_type type_of(hol_term tm);

Returns the type of a term.

• raises — Never fails.

type_substtype_subst takes a list of hol_type_pairhol_type_pair, each pairing a replacement type with the type variable it replaces; the same pair-list type is what inst_type_ruleinst_type_rule consumes on HOL API: Inference Rules. Equality of types is equals_typeequals_type, documented with the other comparison functions at the end of this page.

A HOL term is a variable, a constant, a combination (application) or an abstraction. Those four are the whole term language. Every other form named below — conjunction, universal quantification, a numeral, a list — is a constant applied to arguments, and the corresponding mk_mk_ / dest_dest_ / is_is_ triple is a view of that shape rather than a new kind of term.

The naming is HOL Light’s throughout: mk_mk_ constructs, dest_dest_ destructs, is_is_ tests, list_mk_list_mk_ iterates a binary constructor over a list, and strip_strip_ iterates the matching destructor. Constructors type-check, so mk_combmk_comb fails on a type mismatch and mk_conjmk_conj fails on a non-boolean argument; destructors fail on the wrong shape; tests never fail.

hol_term mk_var(const_cstr s, hol_type ty);

hol_term mk_var(const_cstr s, hol_type ty);

Constructs a variable of given name and type.

• raises — Never fails.

dest_var_results dest_var(hol_term tm);

dest_var_results dest_var(hol_term tm);

Breaks apart a variable into name and type.

• raises — Fails if the term is not a variable.

hol_term mk_const(const_cstr s, hol_type ty);

hol_term mk_const(const_cstr s, hol_type ty);

Constructs a constant with type matching.

• raises — Fails if the string supplied is not the name of a known constant, or if it is known but the type supplied is not the correct type for the constant.

hol_term mk_iconst(const_cstr s, hol_type_pair_list ty_pairs);

hol_term mk_iconst(const_cstr s, hol_type_pair_list ty_pairs);

Produce constant term by applying an instantiation to its generic type.

• raises — Fails if there is no constant of the given type.

dest_const_results dest_const(hol_term tm);

dest_const_results dest_const(hol_term tm);

Breaks apart a constant into name and type.

• raises — Fails if the term is not a constant.

hol_term mk_comb(hol_term tm1, hol_term tm2);

hol_term mk_comb(hol_term tm1, hol_term tm2);

Constructs a combination.

• raises — Fails if the types of the terms are not compatible.

hol_term list_mk_comb(hol_term tm, hol_term_list tms);

hol_term list_mk_comb(hol_term tm, hol_term_list tms);

Iteratively constructs combinations (function applications).

• raises — Fails if the types of the argument types are not equal to the parameter types.

dest_comb_results dest_comb(hol_term tm);

dest_comb_results dest_comb(hol_term tm);

Breaks apart a combination (function application) into rator and rand.

• raises — Fails if the term is not a combination.

hol_term get_operand(hol_term tm);

hol_term get_operand(hol_term tm);

Returns the operand from a combination (function application).

• raises — Fails if the term is not a combination.

hol_term get_operator(hol_term tm);

hol_term get_operator(hol_term tm);

Returns the operator from a combination (function application).

• raises — Fails if the term is not a combination.

strip_comb_results strip_comb(hol_term tm);

strip_comb_results strip_comb(hol_term tm);

Iteratively breaks apart combinations (function applications).

• raises — Never fails.

hol_term mk_abs(hol_term v, hol_term tm);

hol_term mk_abs(hol_term v, hol_term tm);

Constructs an abstraction.

• raises — Fails if the first term is not a variable.

hol_term list_mk_abs(hol_term_list vs, hol_term tm);

hol_term list_mk_abs(hol_term_list vs, hol_term tm);

Iteratively constructs abstractions.

• raises — Fails if the terms in the list are not variables.

dest_abs_results dest_abs(hol_term tm);

dest_abs_results dest_abs(hol_term tm);

Breaks apart an abstraction into abstracted variable and body.

• raises — Fails if the term is not an abstraction.

hol_term bvar(hol_term tm);

hol_term bvar(hol_term tm);

Returns the bound variable of an abstraction.

• raises — Fails if the term is not an abstraction.

hol_term body(hol_term tm);

hol_term body(hol_term tm);

Returns the body of an abstraction.

• raises — Fails if the term is not an abstraction.

strip_abs_results strip_abs(hol_term tm);

strip_abs_results strip_abs(hol_term tm);

Iteratively breaks apart abstractions.

• raises — Never fails.

get_operatorget_operator and get_operandget_operand are the two projections of dest_combdest_comb, useful when only one half is wanted; bvarbvar and bodybody play the same role for dest_absdest_abs. mk_iconstmk_iconst differs from mk_constmk_const in how the constant’s type is fixed: mk_constmk_const is given the instance type outright, mk_iconstmk_iconst a type instantiation to apply to the constant’s generic type.

Below the specific families sits a generic layer that works for any constant used infix or as a binder. This is how a term built from a C* constant — ****, |--|--, a user-defined predicate — is inspected without a dedicated destructor.

hol_term mk_binary(const_cstr s, hol_term tm1, hol_term tm2);

hol_term mk_binary(const_cstr s, hol_term tm1, hol_term tm2);

Constructs an instance of a named monomorphic binary operator.

• raises — Fails if there is no constant at all with the given name, or if the constant is polymorphic and the terms do not match its most general type.

dest_binary_results dest_binary(const_cstr s, hol_term tm);

dest_binary_results dest_binary(const_cstr s, hol_term tm);

Breaks apart an instance of a binary operator with given name.

• raises — Fails if the given term is not an instance of a binary operator with given name.

bool is_binary(const_cstr s, hol_term tm);

bool is_binary(const_cstr s, hol_term tm);

Tests if a term is an application of a named binary operator.

• raises — Never fails.

hol_term mk_binder(const_cstr s, hol_term v, hol_term tm);

hol_term mk_binder(const_cstr s, hol_term v, hol_term tm);

Constructs a term with a named constant applied to an abstraction.

• raises — Fails if the first term is not a variable, if there is no constant of the given name, or if the type of that constant cannot be instantiated to match the abstraction.

dest_binder_results dest_binder(const_cstr s, hol_term tm);

dest_binder_results dest_binder(const_cstr s, hol_term tm);

Breaks apart a binder.

• raises — Fails if the term is not of the appropriate form with a constant of the same name.

bool is_binder(const_cstr s, hol_term tm);

bool is_binder(const_cstr s, hol_term tm);

Tests if a term is a binder construct with named constant.

• raises — Never fails.

hol_term mk_binop(hol_term op, hol_term tm1, hol_term tm2);

hol_term mk_binop(hol_term op, hol_term tm1, hol_term tm2);

Constructs an instance of a given binary operator.

• raises — Fails if the types are incompatible.

hol_term list_mk_binop(hol_term op, hol_term_list tms);

hol_term list_mk_binop(hol_term op, hol_term_list tms);

Makes an iterative application of a binary operator.

• raises — Fails if the list of terms is empty or if the types would not work for the composite term.

dest_binop_results dest_binop(hol_term op, hol_term tm);

dest_binop_results dest_binop(hol_term op, hol_term tm);

Breaks apart an application of a given binary operator to two arguments.

• raises — Fails if the term is not a binary application of the operator.

hol_term_list strip_binop(hol_term op, hol_term tm);

hol_term_list strip_binop(hol_term op, hol_term tm);

Repeatedly breaks apart an iterated binary operator into components.

• raises — Never fails.

bool is_binop(hol_term op, hol_term tm);

bool is_binop(hol_term op, hol_term tm);

Tests if a term is an application of the given binary operator.

• raises — Never fails.

The binarybinary family identifies the operator by name and the binopbinop family by term, which matters for polymorphic constants: mk_binarymk_binary instantiates the constant’s generic type from its arguments, whereas mk_binopmk_binop takes the already-instantiated operator term.

hol_term mk_true();

hol_term mk_true();

The true constant.

• raises — Never fails.

hol_term mk_false();

hol_term mk_false();

The false constant.

• raises — Never fails.

hol_term mk_conj(hol_term tm1, hol_term tm2);

hol_term mk_conj(hol_term tm1, hol_term tm2);

Constructs a conjunction.

• raises — Fails if either term is not of type bool.

hol_term list_mk_conj(hol_term_list tms);

hol_term list_mk_conj(hol_term_list tms);

Constructs the conjunction of a list of terms.

• raises — Fails if the list is empty or if the list has more than one element, one or more of which are not of type bool.

dest_conj_results dest_conj(hol_term tm);

dest_conj_results dest_conj(hol_term tm);

Term destructor for conjunctions.

• raises — Fails if the term is not a conjunction.

hol_term_list strip_conj(hol_term tm);

hol_term_list strip_conj(hol_term tm);

Iteratively breaks apart a conjunction.

• raises — Never fails.

hol_term mk_imp(hol_term tm1, hol_term tm2);

hol_term mk_imp(hol_term tm1, hol_term tm2);

Constructs an implication.

• raises — Fails if either term is not of type bool.

dest_imp_results dest_imp(hol_term tm);

dest_imp_results dest_imp(hol_term tm);

Breaks apart an implication into antecedent and consequent.

• raises — Fails if the term is not an implication.

hol_term mk_disj(hol_term tm1, hol_term tm2);

hol_term mk_disj(hol_term tm1, hol_term tm2);

Constructs a disjunction.

• raises — Fails if either term is not of type bool.

hol_term list_mk_disj(hol_term_list tms);

hol_term list_mk_disj(hol_term_list tms);

Constructs the disjunction of a list of terms.

• raises — Fails if the list is empty or if the list has more than one element, one or more of which are not of type bool.

dest_disj_results dest_disj(hol_term tm);

dest_disj_results dest_disj(hol_term tm);

Breaks apart a disjunction into the two disjuncts.

• raises — Fails if the term is not a disjunction.

hol_term_list strip_disj(hol_term tm);

hol_term_list strip_disj(hol_term tm);

Iteratively breaks apart a disjunction.

• raises — Never fails.

hol_term mk_not(hol_term tm);

hol_term mk_not(hol_term tm);

Constructs a logical negation.

• raises — Fails if the term is not of type bool.

hol_term dest_not(hol_term tm);

hol_term dest_not(hol_term tm);

Breaks apart a negation, returning its body.

• raises — Fails if the term is not a negation.

The quantifier constructors take the bound variable as a term and reject anything that is not a variable. list_mk_foralllist_mk_forall and strip_forallstrip_forall handle a whole prefix of quantifiers at once, which is what proof code normally wants when specialising a stored theorem.

hol_term mk_forall(hol_term v, hol_term tm);

hol_term mk_forall(hol_term v, hol_term tm);

Term constructor for universal quantification.

• raises — Fails if the first term is not a variable or if the second term is not of type bool.

hol_term list_mk_forall(hol_term_list vs, hol_term tm);

hol_term list_mk_forall(hol_term_list vs, hol_term tm);

Iteratively constructs a universal quantification.

• raises — Fails if any term in the list is not a variable or if the second term is not of type bool and the list of terms is non-empty.

dest_forall_results dest_forall(hol_term tm);

dest_forall_results dest_forall(hol_term tm);

Breaks apart a universally quantified term into quantified variable and body.

• raises — Fails if the term is not a universal quantification.

strip_forall_results strip_forall(hol_term tm);

strip_forall_results strip_forall(hol_term tm);

Iteratively breaks apart universal quantifications.

• raises — Never fails.

hol_term mk_exists(hol_term v, hol_term tm);

hol_term mk_exists(hol_term v, hol_term tm);

Term constructor for existential quantification.

• raises — Fails if the first term is not a variable or if the second term is not of type bool.

hol_term list_mk_exists(hol_term_list vs, hol_term tm);

hol_term list_mk_exists(hol_term_list vs, hol_term tm);

Iteratively constructs an existential quantification.

• raises — Fails if any term in the list is not a variable or if the second term is not of type bool and the list of terms is non-empty.

dest_exists_results dest_exists(hol_term tm);

dest_exists_results dest_exists(hol_term tm);

Breaks apart an existentially quantified term into quantified variable and body.

• raises — Fails if the term is not an existential quantification.

strip_exists_results strip_exists(hol_term tm);

strip_exists_results strip_exists(hol_term tm);

Iteratively breaks apart existential quantifications.

• raises — Never fails.

hol_term mk_uexists(hol_term v, hol_term tm);

hol_term mk_uexists(hol_term v, hol_term tm);

Term constructor for unique existence.

• raises — Fails if the first term is not a variable or if the second term is not of type bool.

dest_uexists_results dest_uexists(hol_term tm);

dest_uexists_results dest_uexists(hol_term tm);

Breaks apart a unique existence term.

• raises — Fails if the term is not a unique existence term.

hol_term mk_let(hol_term_pair_list tm_pairs, hol_term tm);

hol_term mk_let(hol_term_pair_list tm_pairs, hol_term tm);

Constructs a let-expression.

• raises — Fails if the list of left-hand and right-hand sides is empty or if some corresponding pair of left-hand and right-hand sides have different types.

dest_let_results dest_let(hol_term tm);

dest_let_results dest_let(hol_term tm);

Breaks apart a let-expression.

• raises — Fails if the term is not a let-expression.

hol_term mk_select(hol_term v, hol_term tm);

hol_term mk_select(hol_term v, hol_term tm);

Constructs a choice binding.

• raises — Fails if the first term is not a variable.

dest_select_results dest_select(hol_term tm);

dest_select_results dest_select(hol_term tm);

Breaks apart a choice term into selected variable and body.

• raises — Fails if the term is not an epsilon-term.

mk_eqmk_eq builds an equation at any type and mk_iffmk_iff is its boolean case — in HOL Light both are the same constant, so is_eqis_eq holds of an equivalence too. dest_iffdest_iff is the destructor that insists on boolean operands.

hol_term mk_eq(hol_term tm1, hol_term tm2);

hol_term mk_eq(hol_term tm1, hol_term tm2);

Constructs an equation.

• raises — Fails if the two terms have different types.

dest_eq_results dest_eq(hol_term tm);

dest_eq_results dest_eq(hol_term tm);

Term destructor for equality.

• raises — Fails if the term is not an equality.

hol_term mk_cond(hol_term tm1, hol_term tm2, hol_term tm3);

hol_term mk_cond(hol_term tm1, hol_term tm2, hol_term tm3);

Constructs a conditional term.

• raises — Fails if the first term is not of type bool or if last two terms are of different types.

dest_cond_results dest_cond(hol_term tm);

dest_cond_results dest_cond(hol_term tm);

Breaks apart a conditional into the three terms involved.

• raises — Fails if the term is not a conditional.

hol_term mk_iff(hol_term tm1, hol_term tm2);

hol_term mk_iff(hol_term tm1, hol_term tm2);

Constructs a logical equivalence.

• raises — Fails if either term does not have bool type.

dest_iff_results dest_iff(hol_term tm);

dest_iff_results dest_iff(hol_term tm);

Term destructor for logical equivalence.

• raises — Fails if the term is not a logical equivalence.

A numeric literal is not a primitive term form: a natural-number literal is a numeral term built from the NUMERALNUMERAL constant, and an integer or real literal is a canonical application of the arithmetic constants. The functions here perform that encoding and decoding.

hol_term mk_nat(int i);

hol_term mk_nat(int i);

Maps a nonnegative integer to corresponding numeral term.

• raises — Fails if the argument is negative.

int dest_nat(hol_term tm);

int dest_nat(hol_term tm);

Converts a numeral term to an integer.

• raises — Fails if the term is not a numeral or if the result doesn't fit in an integer.

hol_term mk_int(int i);

hol_term mk_int(int i);

Converts an integer to a canonical integer literal.

• raises — Never fails.

int dest_int(hol_term tm);

int dest_int(hol_term tm);

Converts an integer literal to an integer.

• raises — Fails if applied to a term that is not a canonical integer literal or if the result doesn't fit in an integer.

hol_term mk_real_int(int i);

hol_term mk_real_int(int i);

Converts an integer to a canonical integer literal of type real.

• raises — Never fails.

hol_term mk_real_rat(int i1, int i2);

hol_term mk_real_rat(int i1, int i2);

Converts a rational number to a canonical rational literal of type real.

• raises — Fails if the denominator is zero.

int dest_real_int(hol_term tm);

int dest_real_int(hol_term tm);

Converts an integer literal of type real to an integer.

• raises — Fails if applied to a term that is not a canonical integer literal of type real.

dest_real_rat_results dest_real_rat(hol_term tm);

dest_real_rat_results dest_real_rat(hol_term tm);

Converts a canonical rational literal of type real to a rational number.

• raises — Fails when applied to a term that is not a canonical rational literal of if the result doesn't fit in an integer.

hol_term mk_string(const_cstr s);

hol_term mk_string(const_cstr s);

Constructs object-level string from a literal string.

• raises — Never fails.

cstr dest_string(hol_term tm);

cstr dest_string(hol_term tm);

Produces a literal string corresponding to object-level string.

• raises — Fails if the term is not a literal term of type string.

long long dest_nat64(hol_term tm);

long long dest_nat64(hol_term tm);

Converts a numeral term to an integer.

• raises — Fails if the term is not a numeral or if the result doesn't fit in an integer.

long long dest_int64(hol_term tm);

long long dest_int64(hol_term tm);

Converts an integer literal to an integer.

• raises — Fails if applied to a term that is not a canonical integer literal or if the result doesn't fit in an integer.

dest_nat64dest_nat64 and dest_int64dest_int64 are the long longlong long variants of dest_natdest_nat and dest_intdest_int, for literals outside the range of a C intint — the magnitudes that appear routinely in C* specifications about 64-bit machine values.

hol_term mk_pair(hol_term tm1, hol_term tm2);

hol_term mk_pair(hol_term tm1, hol_term tm2);

Constructs object-level pair from a pair of terms.

• raises — Never fails.

hol_term list_mk_pair(hol_term_list tms);

hol_term list_mk_pair(hol_term_list tms);

Constructs the tuple of a list of terms.

• raises — Fails if the list is empty.

dest_pair_results dest_pair(hol_term tm);

dest_pair_results dest_pair(hol_term tm);

Breaks apart a pair into two separate terms.

• raises — Fails if the term is not a pair.

hol_term_list strip_pair(hol_term tm);

hol_term_list strip_pair(hol_term tm);

Iteratively breaks apart a tuple.

• raises — Never fails.

hol_term mk_list(hol_term_list tms, hol_type ty);

hol_term mk_list(hol_term_list tms, hol_type ty);

Constructs object-level list from list of terms.

• raises — Fails if any term in the list is not of the type specified as the second argument.

hol_term mk_nil(hol_type ty);

hol_term mk_nil(hol_type ty);

Constructs a nil list.

• raises — Never fails.

hol_term mk_cons(hol_term tm1, hol_term tm2);

hol_term mk_cons(hol_term tm1, hol_term tm2);

Constructs a cons list.

• raises — Fails if the second term is not of list type or if the first term is not of the same type as the elements of the list.

dest_cons_results dest_cons(hol_term tm);

dest_cons_results dest_cons(hol_term tm);

Breaks apart a cons list into head and tail.

• raises — Fails if the term is not a non-empty list.

hol_term_list dest_list(hol_term tm);

hol_term_list dest_list(hol_term tm);

Iteratively breaks apart a list term.

• raises — Fails if the term is not a list.

mk_listmk_list needs the element type explicitly because the empty list is polymorphic; mk_nilmk_nil is the same construction with zero elements.

Every family above has a test that never fails and returns falsefalse for a term of any other shape:

is_boolis_bool is the odd one out: it tests whether a term is a constant of type :bool:bool — that is, TT or FF — not whether the term has boolean type. Use equals_type(type_of(tm), mk_bool_type())equals_type(type_of(tm), mk_bool_type()) for the latter.

These are the operations proof code reaches for when it has to manufacture a fresh name, avoid a capture, or compare two terms up to bound-variable renaming.

int alpha_compare(hol_term tm1, hol_term tm2);

int alpha_compare(hol_term tm1, hol_term tm2);

Total ordering on terms respecting alpha-equivalence.

• raises — Never fails.

hol_term_list free_vars(hol_term tm);

hol_term_list free_vars(hol_term tm);

Returns a list of the variables free in a term.

• raises — Never fails.

hol_term_list list_free_vars(hol_term_list tms);

hol_term_list list_free_vars(hol_term_list tms);

Returns a list of the free variables in a list of terms.

• raises — Never fails.

bool free_vars_in(hol_term tm, hol_term_list vs);

bool free_vars_in(hol_term tm, hol_term_list vs);

Tests if all free variables of a term appear in a list.

• raises — Never fails.

bool var_free_in(hol_term v, hol_term tm);

bool var_free_in(hol_term v, hol_term tm);

Tests whether a variable (or constant) occurs free in a term.

• raises — Never fails.

hol_type_list term_tyvars(hol_term tm);

hol_type_list term_tyvars(hol_term tm);

Returns the set of type variables used in a term.

• raises — Never fails.

hol_term variant(hol_term_list tms, hol_term v);

hol_term variant(hol_term_list tms, hol_term v);

Modifies a variable name to avoid clashes.

• raises — Fails if any term in the list is not a variable or if the given term is neither a variable nor a constant.

hol_term subst(hol_term_pair_list tm_pairs, hol_term tm);

hol_term subst(hol_term_pair_list tm_pairs, hol_term tm);

Substitute terms for other terms inside a term.

• raises — Fails if any of the pairs in the instantiation list has different types.

hol_term tyvar_inst(hol_type_pair_list ty_pairs, hol_term tm);

hol_term tyvar_inst(hol_type_pair_list ty_pairs, hol_term tm);

Instantiate type variables in a term.

• raises — Never fails.

hol_term genvar(hol_type ty);

hol_term genvar(hol_type ty);

Returns a fresh variable with specified type.

• raises — Never fails.

hol_term_list variants(hol_term_list av, hol_term_list vs);

hol_term_list variants(hol_term_list av, hol_term_list vs);

Pick a list of variants of variables, avoiding a list of variables and each other.

• raises — Fails if any of the terms in the list is not a variable.

variantvariant and variantsvariants are the standard way to obtain names that do not clash with terms already in play, and genvargenvar produces a name that cannot clash with anything a user wrote. substsubst substitutes terms for terms and requires each pair to be type-compatible; tyvar_insttyvar_inst substitutes types for type variables throughout a term.

The last group compares two syntactic objects, or matches one against another. The header declares all six of these far later in the file, among the inference rules and the conversions, because that is where their implementations sit; they are documented here because what they operate on is syntax, not proof.

bool equals_type(hol_type ty1, hol_type ty2);

bool equals_type(hol_type ty1, hol_type ty2);

Equality test on types.

• raises — Never fails.

bool equals_term(hol_term tm1, hol_term tm2);

bool equals_term(hol_term tm1, hol_term tm2);

Equality test on terms.

• raises — Never fails.

bool equals_thm(hol_theorem th1, hol_theorem th2);

bool equals_thm(hol_theorem th1, hol_theorem th2);

Equality test on theorems.

• raises — Never fails.

hol_instantiation term_match(hol_term_list tms, hol_term tm1, hol_term tm2);

hol_instantiation term_match(hol_term_list tms, hol_term tm1, hol_term tm2);

Match one term against another. The call term_match lcs t t'term_match lcs t t' attempts to find an instantiation for free variables in tt, not permitting assignment of local constant variables in the list lcslcs, so that it is alpha-equivalent to t't'.

• raises — Fails if terms cannot be matched.

hol_term instantiate(hol_instantiation inst, hol_term tm);

hol_term instantiate(hol_instantiation inst, hol_term tm);

Applies a higher-order instantiation to a term.

• raises — Never fails on valid instantiation.

hol_instantiation compose_insts(hol_instantiation i1, hol_instantiation i2);

hol_instantiation compose_insts(hol_instantiation i1, hol_instantiation i2);

Composes two Instantiations.

• raises — Never fails.

equals_typeequals_type, equals_termequals_term and equals_thmequals_thm are syntactic equality — equals_termequals_term is equality of the term structure, so two alpha-equivalent terms are not equal by it and alpha_comparealpha_compare is the test to use instead.

term_matchterm_match is higher-order matching: given a list of term variables to hold fixed, it finds an instantiation that turns the first term into the second, and fails when none exists. The hol_instantiationhol_instantiation it returns is applied to a term by instantiateinstantiate, and to a theorem’s conclusion by instantiate_ruleinstantiate_rule on HOL API: Inference Rules. compose_instscompose_insts composes two such instantiations, which is how a matching step is chained onto one already computed.

The API on this page is HOL Light’s syntax layer exposed as C. Types are variables or applied constructors; terms are variables, constants, combinations or abstractions; everything else is a named view of those shapes, presented as a mk_mk_ / dest_dest_ / is_is_ triple with list_mk_list_mk_ and strip_strip_ for the iterated forms. Constructors type-check and can fail, destructors fail on the wrong shape, tests never fail, and every failure is visible through get_last_status()get_last_status() while the returned value is an empty_*empty_* sentinel rather than NULLNULL.

None of this proves anything. A term is a syntactic object with no truth attached; only a hol_theoremhol_theorem carries a claim, and the only ways to obtain one are from the theory or from an inference rule.