HOL API：类型与项

hol_prover_client.hhol_prover_client.h 是 HOL Light 的一层轻量 RPC 客户端。其中每个函数都对应证明器在自己进程中执行的一项操作，并交回一个指向证明器所创建对象的不透明句柄。因此，用 mk_combmk_comb 构造一个项并非本地的内存分配，而是一次请求：证明器对它做类型检查，随后接受或拒绝。

以下四条约定适用于本页以及随后三页中的每一条声明。

• 每次调用都会记录状态。 任何调用之后，get_last_status()get_last_status() 的取值为 HOL_STATUS_OKHOL_STATUS_OK 或 HOL_STATUS_ERRORHOL_STATUS_ERROR，后者的具体信息由 get_last_error()get_last_error() 给出。检查状态是推荐的做法：它对返回 boolbool、intint 或 voidvoid 的函数同样统一适用，而这些函数并没有专门的失败返回值。
• 调用失败返回 empty_*empty_* 哨兵值，绝不返回 NULLNULL。 头文件声明了 empty_termempty_term、empty_theoremempty_theorem、empty_typeempty_type、empty_conversionempty_conversion 以及相应的成对值。检测结果应使用通用宏 IS_NULLIS_NULL，而不是与 NULLNULL 比较——这些对象类型是结构体，并非指针。空列表是长度为零的向量，是完全合法的值；列表指针为空才表示出错。
• 所有返回的指针都由垃圾回收管理。 每一个 cstrcstr、每一个列表以及每个句柄背后的内存，都由运行时链接进来的 GC 管理。本 API 返回的任何东西都不需要调用方释放，而 get_last_error()get_last_error() 返回的 const char*const char* 可能在下一次调用后失效。
• 头文件是生成的，请勿编辑。 其中的声明来自证明器自身的接口描述，因此文档注释读起来很像 HOL Light 的参考手册。本页逐字重现这些注释，并一并给出头文件所声明的失败条件。

连接是进程级的。hol_prover_init()hol_prover_init() 负责建立连接；hol_prover_shutdown()hol_prover_shutdown() 拆除连接并重置状态，此后可以在同一进程中用 hol_prover_init()hol_prover_init() 建立一条新的连接。

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.

状态本身只是一个普通的 intint（typedef int hol_status_ttypedef int hol_status_t），有两个见于文档的取值：

四种对象类型都是不透明结构体，各自包裹一个客户端不得触碰的指针：

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;

由于它们是结构体而非指针，调用失败时无法靠返回 NULLNULL 来表示失败，而是返回一个 innerinner 字段为空的哨兵值——empty_termempty_term、empty_theoremempty_theorem、empty_typeempty_type、empty_conversionempty_conversion，成对的结果则对应 empty_term_pairempty_term_pair、empty_thm_pairempty_thm_pair、empty_type_pairempty_type_pair。头文件为它们提供了统一的判别宏：

#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

在 C 中它是一次 _Generic_Generic 选择；在 C++ 中同名的是一组重载。两者都接受 charchar、char*char*、const char*const char* 以及四种对象类型中的任意一种，因此返回的字符串也应当用 IS_NULLIS_NULL 来检测。其余的检测宏覆盖各种聚合值：

列表是向量，并非以空指针结尾的数组。hol_term_listhol_term_list、hol_type_listhol_type_list、hol_theorem_listhol_theorem_list、cstr_listcstr_list、int_listint_list 以及各种成对列表类型，都是指向向量存储的 T*T*，长度保存在向量之中，而不是靠结尾标记。空列表是合法的值，用 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.

有几个解构函数会返回多个值，头文件为每一个都声明了一个小的结果结构体——dest_app_type_resultsdest_app_type_results、dest_comb_resultsdest_comb_results、strip_forall_resultsstrip_forall_results、dest_thm_resultsdest_thm_results 等等。它们都是带具名字段的普通结构体，各自出现在产生它的那个函数的声明中。

一个 HOL 类型要么是类型变量，要么是作用于一组参数类型的类型构造子。其余一切——函数类型、积类型、列表类型——都是名字固定的构造子；头文件在 mk_app_typemk_app_type 与 dest_app_typedest_app_type 之上，为常用的几种提供了一层便捷封装。

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.

基本类型各有一个零元构造函数，都不会失败：

函数类型是最常用的一类。list_mk_fun_typelist_mk_fun_type 与 strip_fun_typestrip_fun_type 处理柯里化形式，因此像 :num->num->bool:num->num->bool 这样的谓词类型，可以一次调用构造出来，也可以一次调用拆开。

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.

积类型与列表类型遵循同样的构造 / 迭代 / 解构 / 剥离模式：

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.

每一族都有对应的判别函数，且判别函数都不会失败——遇到其他形状的类型，只会返回 falsefalse：

最后是把类型与项、以及类型彼此关联起来的操作：

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 接受一个 hol_type_pairhol_type_pair 列表，其中每一对把替换用的类型与被替换的类型变量配在一起；HOL API：推理规则中的 inst_type_ruleinst_type_rule 所消耗的正是同一种成对列表类型。类型的相等用 equals_typeequals_type，它与其他比较函数一起记录在本页末尾。

一个 HOL 项是变量、常量、组合（应用）或抽象。这四者构成了完整的项语言。下面提到的其他一切形式——合取、全称量化、数字、列表——都是常量作用于参数的结果，对应的 mk_mk_ / dest_dest_ / is_is_ 三件套只是对这种形状的一种视角，并未引入新的项种类。

命名一律沿用 HOL Light 的做法：mk_mk_ 构造，dest_dest_ 解构，is_is_ 判别，list_mk_list_mk_ 把一个二元构造函数沿列表迭代，strip_strip_ 迭代与之对应的解构函数。构造函数会做类型检查，因此 mk_combmk_comb 在类型不匹配时失败，mk_conjmk_conj 在参数不是布尔类型时失败；解构函数在形状不对时失败；判别函数从不失败。

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 与 get_operandget_operand 是 dest_combdest_comb 的两个投影，只需要其中一半时很方便；bvarbvar 与 bodybody 对 dest_absdest_abs 起同样的作用。mk_iconstmk_iconst 与 mk_constmk_const 的区别在于常量类型的确定方式：mk_constmk_const 直接给出实例类型，mk_iconstmk_iconst 给出的则是作用于该常量泛型类型的一个类型实例化。

在这些具体的函数族之下，还有一层通用接口，适用于任何以中缀方式使用或作为绑定子使用的常量。由 C* 常量——****、|--|--、用户自定义谓词——构造出的项，正是靠它在没有专用解构函数的情况下得以检视。

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.

binarybinary 一族按名字标识运算符，binopbinop 一族按项标识，这对多态常量很重要：mk_binarymk_binary 根据参数实例化常量的泛型类型，而 mk_binopmk_binop 接受的是已经实例化好的运算符项。

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.

量词构造函数以项的形式接受被绑定的变量，凡不是变量的一律拒绝。list_mk_foralllist_mk_forall 与 strip_forallstrip_forall 一次处理整串量词前缀，证明代码在特化一条已存定理时通常正需要这种方式。

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 在任意类型上构造等式，mk_iffmk_iff 是它的布尔特例——在 HOL Light 中两者是同一个常量，因此 is_eqis_eq 对等价式同样成立。dest_iffdest_iff 则是要求操作数必须为布尔类型的解构函数。

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.

数值字面量并非原始的项形式：自然数字面量是由 NUMERALNUMERAL 常量构造出的数字项，整数或实数字面量则是算术常量的一种规范应用。这里的函数负责相应的编码与解码。

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 与 dest_int64dest_int64 是 dest_natdest_nat 和 dest_intdest_int 的 long longlong long 版本，用于超出 C intint 表示范围的字面量——在关于 64 位机器值的 C* 规约中，这种量级十分常见。

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 需要显式给出元素类型，因为空列表是多态的；mk_nilmk_nil 则是元素个数为零时的同一种构造。

上面每一族都有一个判别函数，它从不失败，遇到任何其他形状的项都返回 falsefalse：

is_boolis_bool 是其中的例外：它判别的是项是否为类型 :bool:bool 的常量（也就是 TT 或 FF），并非该项是否具有布尔类型。后者应当用 equals_type(type_of(tm), mk_bool_type())equals_type(type_of(tm), mk_bool_type())。

当证明代码需要生成一个新名字、避免变量捕获，或在绑定变量重命名的意义下比较两个项时，用到的就是这一组操作。

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 和 variantsvariants；genvargenvar 生成的名字则不可能与用户写下的任何名字冲突。substsubst 以项替换项，要求每一对在类型上相容；tyvar_insttyvar_inst 在整个项中以类型替换类型变量。

最后一组用于比较两个语法对象，或把一个与另一个做匹配。头文件把这六个函数的声明放在文件靠后的位置，夹在推理规则与变换之间，因为它们的实现就在那里；这里记录它们，是因为它们操作的对象是语法，而非证明。

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 与 equals_thmequals_thm 都是语法上的相等——equals_termequals_term 比较的是项的结构，因此两个 α-等价的项在它看来并不相等，这时应改用 alpha_comparealpha_compare。

term_matchterm_match 是高阶匹配：给定一组需要保持固定的项变量，它寻找一个把第一个项变为第二个项的实例化，找不到时失败。它返回的 hol_instantiationhol_instantiation 由 instantiateinstantiate 作用到项上，由HOL API：推理规则中的 instantiate_ruleinstantiate_rule 作用到定理的结论上。compose_instscompose_insts 把两个这样的实例化复合起来，一次匹配步骤正是这样接到已经算好的实例化之后。

本页的 API 就是 HOL Light 的语法层以 C 的形式开放出来。类型是类型变量，或是作用于参数的构造子；项是变量、常量、组合或抽象；其余一切都是这些形状的具名视角，以 mk_mk_ / dest_dest_ / is_is_ 三件套呈现，迭代形式则由 list_mk_list_mk_ 与 strip_strip_ 承担。构造函数会做类型检查，可能失败；解构函数在形状不对时失败；判别函数从不失败；每一次失败都可以通过 get_last_status()get_last_status() 看到，而返回值是 empty_*empty_* 哨兵值，并非 NULLNULL。

这一切都不证明任何东西。项是不附带真值的语法对象；只有 hol_theoremhol_theorem 才承载一项断言，而获得它的途径只有两条：从理论中取得，或由推理规则导出。