kernel API 参考

kernel 包（Luna-Flow/QED/kernel）是 QED 的可信内核。它定义 HOL 类型与项、抽象定理类型 Thm、作为构造 Thm 唯一途径的原始推理规则、带作用域的签名，以及三个扩张闸门 DefOK、TypeDefOK 和 SpecOK。它不依赖任何其他 QED 包。其他所有包只能通过本页的函数获得定理。

失败是值：规则返回 Result[Thm, LogicError]，签名操作返回 Result[_, SigError]。本页中没有任何操作会因错误输入而中止。

本页的示例是以 @kernel 导入该包的黑盒测试。规则的含义在内核设计说明中解释；内核教程提供了引导式讲解。规范性的定义见形式化规范：

QED 形式化规范

类型

HolType

HolType 是简单类型：类型变量，或应用于若干参数的类型构造子。

pub enum HolType {
  TyVal(String)
  TyApp(String, Array[HolType])
}

TyVal(a) 是名为 a 的类型变量 $\alpha$。TyApp(c, args) 把构造子 c 应用于 args。内置构造子有 bool（元数 0）、ind（元数 0）和 fun（元数 2）；fun(a, b) 是函数类型 $a \to b$。其他构造子只有在 ks_register_type_definition 接纳之后才可使用。该枚举在包外只读：可以对它做匹配，但应使用下列函数构造值。

mk_tyvar

mk_tyvar 构造给定名称的类型变量。

pub fn mk_tyvar(String) -> HolType

mk_tyapp

mk_tyapp 把类型构造子应用于参数列表。

pub fn mk_tyapp(String, Array[HolType]) -> HolType

结果不依据签名检查。ks_type_is_admissible 判定某个状态是否接受它。

bool_ty、ind_ty 和 fun_ty

这些函数构造三个内置类型：bool_ty() 是 bool，ind_ty() 是无限的个体类型 ind，fun_ty(a, b) 是 $a \to b$。

pub fn bool_ty() -> HolType
pub fn ind_ty() -> HolType
pub fn fun_ty(HolType, HolType) -> HolType

dest_tyapp 和 dest_fun_ty

dest_tyapp 返回类型应用的构造子和参数，dest_fun_ty 返回函数类型的定义域和值域。对其他形状，两者都返回 None。

pub fn dest_tyapp(HolType) -> (String, Array[HolType])?
pub fn dest_fun_ty(HolType) -> (HolType, HolType)?

is_bool_ty、is_tyvar 和 is_tyapp

这些谓词测试类型的形状。

pub fn is_bool_ty(HolType) -> Bool
pub fn is_tyvar(HolType) -> Bool
pub fn is_tyapp(HolType) -> Bool

ty_eq

ty_eq 是类型的结构相等。

pub fn ty_eq(HolType, HolType) -> Bool

tyvars 和 tyvars_subset

tyvars 按首次出现的顺序列出类型的类型变量，不含重复。当 a 的每个类型变量都出现在 b 中时，tyvars_subset(a, b) 成立。

pub fn tyvars(HolType) -> Array[String]
pub fn tyvars_subset(HolType, HolType) -> Bool

ty_is_instance_of

当存在类型代换 $\theta$ 把 schema 映射为 instance，即 $\mathit{schema}\,\theta = \mathit{instance}$ 时，ty_is_instance_of(instance, schema) 成立。

pub fn ty_is_instance_of(HolType, HolType) -> Bool

注意参数顺序：实例在前。内核用这个关系，把多态常量的每一次出现与其声明的模式相核对。

type_subst、type_subst_unsafe 和 has_duplicate_ty_subst_keys

type_subst(theta, ty) 把类型代换 theta（以类型变量名与类型的对给出）应用于 ty。当 theta 两次给出同一个变量时返回 None，该情况由 has_duplicate_ty_subst_keys 检测。type_subst_unsafe 跳过该检查，并对重复的名称使用第一个绑定。

pub fn type_subst(Array[(String, HolType)], HolType) -> HolType?
pub fn type_subst_unsafe(Array[(String, HolType)], HolType) -> HolType
pub fn has_duplicate_ty_subst_keys(Array[(String, HolType)]) -> Bool

hol_type_to_string

hol_type_to_string 为测试和诊断渲染类型：A、bool、fun(A, bool)。

pub fn hol_type_to_string(HolType) -> String

test "types" {
  let a = @kernel.mk_tyvar("A")
  let pred = @kernel.fun_ty(a, @kernel.bool_ty())
  inspect(@kernel.hol_type_to_string(pred), content="fun(A, bool)")
  inspect(@kernel.dest_fun_ty(pred) is Some((_, cod)) && @kernel.is_bool_ty(cod), content="true")
  assert_eq(@kernel.tyvars(pred), ["A"])
  let inst = @kernel.type_subst([("A", @kernel.ind_ty())], pred).unwrap()
  inspect(@kernel.hol_type_to_string(inst), content="fun(ind, bool)")
  inspect(@kernel.ty_is_instance_of(inst, pred), content="true")
  inspect(@kernel.ty_is_instance_of(pred, inst), content="false")
  inspect(@kernel.type_subst([("A", a), ("A", a)], pred) is None, content="true")
}

项

Term

Term 是简单类型 λ 演算的具名项。

pub enum Term {
  Var(String, HolType)
  Const(String, HolType, Int)
  Comb(Term, Term)
  Abs(Term, Term)
}

Var(x, ty) 是变量；只有名称和类型都一致时，两个变量才相同。Const(c, ty, id) 是常量 c 在类型 ty 上的一次出现；id 是该出现所解析到的常量标识（ConstId），尚未解析时为 -1。Comb(f, x) 是应用 $f\,x$，Abs(v, body) 是抽象 $\lambda v.\,\mathit{body}$，其绑定子 v 必须是 Var。该枚举在包外只读。

mk_var、mk_const、mk_const_bound、mk_comb 和 mk_abs

这些函数不加检查地构造项。mk_const 不解析常量标识（保持 -1）；mk_const_bound 显式设置它。

pub fn mk_var(String, HolType) -> Term
pub fn mk_const(String, HolType) -> Term
pub fn mk_const_bound(String, HolType, Int) -> Term
pub fn mk_comb(Term, Term) -> Term
pub fn mk_abs(Term, Term) -> Term

此处构造的项可能类型错误。type_of 会检查它，且每条规则都会拒绝类型错误的输入。应优先使用 ks_mk_const 和 ks_mk_const_instance，它们从签名中取得类型和标识。

is_var、is_const、is_comb 和 is_abs

这些谓词测试项最外层的构造子。

pub fn is_var(Term) -> Bool
pub fn is_const(Term) -> Bool
pub fn is_comb(Term) -> Bool
pub fn is_abs(Term) -> Bool

dest_var、dest_const、dest_comb 和 dest_abs

这些函数拆解项，对其他形状返回 None。dest_const 会丢弃常量标识。

pub fn dest_var(Term) -> (String, HolType)?
pub fn dest_const(Term) -> (String, HolType)?
pub fn dest_comb(Term) -> (Term, Term)?
pub fn dest_abs(Term) -> (Term, Term)?

type_of

type_of 计算项的类型，项类型错误时返回 None。

pub fn type_of(Term) -> HolType?

它实现简单类型 λ 演算的类型规则：

$$\frac{}{x{:}\tau \vdash x : \tau} \qquad \frac{f : \sigma \to \tau \quad x : \sigma}{f\,x : \tau} \qquad \frac{t : \tau}{\lambda (x{:}\sigma).\,t : \sigma \to \tau}$$

常量具有出现处所写的类型。开销与项的大小成线性关系。

mk_eq 和 dest_eq

mk_eq(l, r) 构造等式 $l = r$，使用类型为 $\tau \to \tau \to \mathit{bool}$ 的内置常量 =。dest_eq 拆解等式。

pub fn mk_eq(Term, Term) -> Result[Term, LogicError]
pub fn dest_eq(Term) -> Result[(Term, Term), LogicError]

当某一边类型错误或两边类型不同时，mk_eq 以 TypeMismatch 失败；当某一边无法转换为 De Bruijn 形式时（见 to_db_term），以 BoundaryFailure 失败。当项不是 = 应用于两个参数时，dest_eq 以 NotAnEquality 失败；当等式类型错误时，以 TypeMismatch 失败。

free_vars、term_is_closed 和 term_has_const_named

free_vars 以名称与类型对的形式列出项的自由变量，不含重复。没有自由变量时 term_is_closed 成立。term_has_const_named 测试给定名称的常量是否在项中的任何位置出现。

pub fn free_vars(Term) -> Array[(String, HolType)]
pub fn term_is_closed(Term) -> Bool
pub fn term_has_const_named(Term, String) -> Bool

term_tyvars 和 term_tyvars_subset

term_tyvars 列出项中任何位置出现的类型变量。当 t 的每个类型变量都出现在 ty 中时，term_tyvars_subset(t, ty) 成立；定义闸门用它来拒绝幽灵类型变量。

pub fn term_tyvars(Term) -> Array[String]
pub fn term_tyvars_subset(Term, HolType) -> Bool

term_apply_ty_subst 和 term_apply_ty_subst_unsafe

这些函数把类型代换应用于项内的每个类型。带检查的形式在某个类型变量被重复给出时返回 None。

pub fn term_apply_ty_subst(Array[(String, HolType)], Term) -> Term?
pub fn term_apply_ty_subst_unsafe(Array[(String, HolType)], Term) -> Term

term_alpha_eq 和 term_logical_eq

term_alpha_eq 判定 α 等价：重命名绑定变量后两个项相等。它比较 De Bruijn 形式，包括常量标识。term_logical_eq 做同样的比较，但忽略常量标识，因此 c 的未解析出现等于已解析出现。当某个项无法转换为 De Bruijn 形式时，两者都返回 false。

pub fn term_alpha_eq(Term, Term) -> Bool
pub fn term_logical_eq(Term, Term) -> Bool

term_to_string

term_to_string 以结构化方式渲染具名项，用于测试和诊断。

pub fn term_to_string(Term) -> String

test "terms" {
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let id_x = @kernel.mk_abs(x, x)
  let id_y = @kernel.mk_abs(y, y)
  inspect(@kernel.hol_type_to_string(@kernel.type_of(id_x).unwrap()), content="fun(A, A)")
  inspect(@kernel.term_alpha_eq(id_x, id_y), content="true")
  inspect(@kernel.free_vars(@kernel.mk_comb(id_x, y)).length(), content="1")
  // applying a function of type A -> A to a bool is ill-typed
  let p = @kernel.mk_var("p", @kernel.bool_ty())
  inspect(@kernel.type_of(@kernel.mk_comb(id_x, p)) is None, content="true")
  let eq = @kernel.mk_eq(x, y).unwrap()
  inspect(
    @kernel.term_to_string(eq),
    content="Comb(Comb(Const(= : fun(A, fun(A, bool))), Var(x : A)), Var(y : A))",
  )
  inspect(@kernel.mk_eq(x, p) is Err(@kernel.TypeMismatch), content="true")
  inspect(@kernel.dest_eq(p) is Err(@kernel.NotAnEquality), content="true")
}

De Bruijn 项

规则运行在带类型的 De Bruijn 表示上，因此 α 等价的项在其中字面相等。这些函数向审计和测试暴露该表示。

DbTerm

DbTerm 是用 De Bruijn 索引表示绑定变量的项。

pub enum DbTerm {
  DbBound(Int, HolType)
  DbFree(String, HolType)
  DbConst(String, HolType, Int)
  DbComb(DbTerm, DbTerm)
  DbAbs(HolType, DbTerm)
}

DbBound(i, ty) 指向向上第 i 层的绑定子，从 0 起计。每个绑定出现都保留其类型，DbAbs(ty, body) 保留绑定子的类型，因此该表示是带类型的。

to_db_term 和 from_db_term

to_db_term 把具名项转换为 De Bruijn 形式；from_db_term 转换回来，选取避开项中自由名称的新绑定名 _b0、_b1、……。

pub fn to_db_term(Term) -> DbTerm?
pub fn from_db_term(DbTerm) -> Term?

当抽象的绑定子不是变量，或某个变量与外层绑定子同名但类型不同（如 $\lambda (x{:}A).\,(x{:}B)$）时，to_db_term 返回 None。QED 拒绝这类项，而不是把内层的 x 当作另一个自由变量。遇到悬空索引或与其绑定子不一致的类型标注时，from_db_term 返回 None。成功时，from_db_term(to_db_term(t)) 与 t α 等价。

db_term_eq、db_type_of 和 db_term_to_string

db_term_eq 是 De Bruijn 项的结构相等，包括常量标识；对转换得到的项，它判定 α 等价。db_type_of 是针对 De Bruijn 项的 type_of。db_term_to_string 渲染 De Bruijn 项，方式同 thm_to_string。

pub fn db_term_eq(DbTerm, DbTerm) -> Bool
pub fn db_type_of(DbTerm) -> HolType?
pub fn db_term_to_string(DbTerm) -> String

db_has_free

db_has_free(t, v) 测试自由变量 v（一个 DbFree）是否在 t 中出现。

pub fn db_has_free(DbTerm, DbTerm) -> Bool

db_subst_free_parallel

db_subst_free_parallel(t, sigma) 同时把每个作为 sigma 键的自由变量替换为其值。值在绑定子之下会被平移，因此不会发生捕获。仅当索引计算会溢出时才返回 None。

pub fn db_subst_free_parallel(DbTerm, Array[(DbTerm, DbTerm)]) -> DbTerm?

db_apply_ty_subst

db_apply_ty_subst 把类型代换应用于 De Bruijn 项的每个类型标注。

pub fn db_apply_ty_subst(Array[(String, HolType)], DbTerm) -> DbTerm

db_beta_reduce_once

db_beta_reduce_once 收缩顶层 β 可约式 $(\lambda.\,t)\,u$，对其他形状返回 None。

pub fn db_beta_reduce_once(DbTerm) -> DbTerm?

收缩为 $\uparrow^{-1}_0\big(t[0 \mapsto \uparrow^{1}_0 u]\big)$：把 u 上移，将其代换到索引 0，再把结果下移。内核设计说明推导了为何这样可避免捕获。

test "de bruijn" {
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let k = @kernel.mk_abs(x, @kernel.mk_abs(y, x)) // λx. λy. x
  let db = @kernel.to_db_term(k).unwrap()
  inspect(@kernel.db_term_to_string(db), content="Abs(A. Abs(A. BVar(1 : A)))")
  // (λx. λy. x) y  reduces to  λ_b. y, not to λy. y
  let redex = @kernel.to_db_term(@kernel.mk_comb(k, y)).unwrap()
  let out = @kernel.db_beta_reduce_once(redex).unwrap()
  inspect(@kernel.db_term_to_string(out), content="Abs(A. FVar(y : A))")
  inspect(
    @kernel.term_to_string(@kernel.from_db_term(out).unwrap()),
    content="Abs(Var(_b0 : A), Var(y : A))",
  )
  // a binder name reused at another type is rejected
  let x_bool = @kernel.mk_var("x", @kernel.bool_ty())
  inspect(@kernel.to_db_term(@kernel.mk_abs(x, x_bool)) is None, content="true")
}

定理

Thm

Thm 是定理的抽象类型：相继式 $\Gamma \vdash p$，带有有限的假设集 $\Gamma$ 和结论 $p$，二者类型均为 bool。

type Thm

该类型是抽象的：包外代码无法构造或修改 Thm。Thm 类型的值之所以存在，只是因为某条原始规则或某个扩张闸门产生了它，这正是内核设计说明中信任论证的全部基础。假设保存为 α 等价类的集合：在 α 等价意义下的重复项会被合并。

thm_hyps、thm_concl 和 thm_hyp_count

thm_hyps 以具名项形式返回假设，thm_concl 返回结论。thm_hyp_count 返回假设的个数。

pub fn thm_hyps(Thm) -> Result[Array[Term], LogicError]
pub fn thm_concl(Thm) -> Result[Term, LogicError]
pub fn thm_hyp_count(Thm) -> Int

绑定变量返回时带有规范名称（_b0、……），因此应使用 term_alpha_eq 或 term_logical_eq 比较结果，而不是做结构比较。对于内核构造的定理，Err(BoundaryFailure) 的情形不会出现。

thm_to_string

thm_to_string 以 De Bruijn 形式把定理渲染为 [h1, h2] |- c。

pub fn thm_to_string(Thm) -> String

thm_is_admissible 和 thm_bind_const_ids

当 th 在 state 中可接受时，thm_is_admissible(state, th) 成立：它提到的每个常量都在该状态中以定理中记录的标识声明，每个常量出现都是其声明模式的实例，每个类型都是可容许的，且定义定理仍与其定义匹配。thm_bind_const_ids 记录 th 中常量在 state 里解析得到的标识，然后检查可容许性。

pub fn thm_is_admissible(KernelState, Thm) -> Bool
pub fn thm_bind_const_ids(KernelState, Thm) -> Result[Thm, LogicError]

每条带检查的规则都对其前提和结果执行此检查，因此在作用域变化前证明的定理，不能在该变化使其某个常量含义改变之后继续使用。当标识与状态不一致时，thm_bind_const_ids 以 InvalidInstantiation 失败；当常量未知时，以 TypeMismatch 失败。

原始规则

每条规则首先接受内核状态，检查其前提定理在该状态中可容许，应用规则，再检查结果。下列规则中，$\Gamma, \Delta$ 是假设集，$\equiv_\alpha$ 是 α 等价（忽略常量标识），$\setminus$ 移除所有与给定项 α 等价的假设。内核设计说明解释了每条规则为何可靠。

refl_checked

refl_checked 是 REFL：它证明一个项等于它自身。

pub fn refl_checked(KernelState, Term) -> Result[Thm, LogicError]

$$\frac{}{\vdash t = t}\;\textsf{REFL}$$

当 t 类型错误或提到状态中未声明的常量时，以 TypeMismatch 失败；当 t 无法转换为 De Bruijn 形式时，以 BoundaryFailure 失败。

assume_checked

assume_checked 是 ASSUME：它由命题自身证明该命题。

pub fn assume_checked(KernelState, Term) -> Result[Thm, LogicError]

$$\frac{p : \mathit{bool}}{\{p\} \vdash p}\;\textsf{ASSUME}$$

当 p 类型良好但类型不是 bool 时，以 NotBoolTerm 失败。

add_assum_checked

add_assum_checked(state, q, th) 把命题 q 加入 th 的假设（弱化）。

pub fn add_assum_checked(KernelState, Term, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash p \qquad q : \mathit{bool}}{\Gamma \cup \{q\} \vdash p}\;\textsf{ADD\_ASSUM}$$

弱化不在规范的十条规则之内；它可由 ASSUME、DEDUCT_ANTISYM_RULE 和 EQ_MP 推导出来，推导见内核设计说明。当 q 不是命题时，以 NotBoolTerm 失败。

trans_checked

trans_checked 是 TRANS：它把两个等式串联起来。

pub fn trans_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash s = t \qquad \Delta \vdash t' = u \qquad t \equiv_\alpha t'}{\Gamma \cup \Delta \vdash s = u}\;\textsf{TRANS}$$

当某个前提不是等式时，以 NotAnEquality 失败；当中间项不同时，以 AlphaMismatch 失败。

mk_comb_rule_checked

mk_comb_rule_checked 是 MK_COMB：相等的函数作用于相等的参数，结果相等。

pub fn mk_comb_rule_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash f = g \qquad \Delta \vdash x = y}{\Gamma \cup \Delta \vdash f\,x = g\,y}\;\textsf{MK\_COMB}$$

除非 $f, g : \sigma \to \tau$ 且 $x, y : \sigma$，否则以 TypeMismatch 失败。

abs_rule_checked

abs_rule_checked(state, x, th) 是 ABS：它对变量抽象等式的两边。

pub fn abs_rule_checked(KernelState, Term, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash s = t \qquad x \notin \mathrm{FV}(\Gamma)}{\Gamma \vdash (\lambda x.\,s) = (\lambda x.\,t)}\;\textsf{ABS}$$

当 x 在某个假设中自由出现时，以 VarFreeInHyp 失败；当 x 不是变量时，以 InvalidInstantiation 失败；当前提不是等式时，以 NotAnEquality 失败。

beta_rule_checked

beta_rule_checked 是 BETA：它证明 β 可约式等于其收缩结果。

pub fn beta_rule_checked(KernelState, Term) -> Result[Thm, LogicError]

$$\frac{u : \sigma}{\vdash (\lambda (x{:}\sigma).\,t)\,u = t[u/x]}\;\textsf{BETA}$$

由于代换在 De Bruijn 项上运行，因此是避免捕获的。当项不是抽象的应用时，以 NotTrivialBetaRedex 失败；当参数类型与绑定子类型不同时，以 TypeMismatch 失败。

eq_mp_checked

eq_mp_checked 是 EQ_MP：命题之间的等式把左边的证明传递到右边。

pub fn eq_mp_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash p = q \qquad \Delta \vdash p' \qquad p \equiv_\alpha p'}{\Gamma \cup \Delta \vdash q}\;\textsf{EQ\_MP}$$

当两边不是命题时，以 NotBoolTerm 失败；当第二个前提没有证明左边时，以 AlphaMismatch 失败。

deduct_antisym_rule_checked

deduct_antisym_rule_checked 是 DEDUCT_ANTISYM_RULE：互相可证的两个命题相等。

pub fn deduct_antisym_rule_checked(KernelState, Thm, Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash p \qquad \Delta \vdash q}{(\Gamma \setminus \{q\}) \cup (\Delta \setminus \{p\}) \vdash p = q}\;\textsf{DEDUCT\_ANTISYM\_RULE}$$

当某个结论不是命题时，以 NotBoolTerm 失败。

inst_type

inst_type(state, theta, th) 是 INST_TYPE：它在整个定理中实例化类型变量。

pub fn inst_type(KernelState, Array[(String, HolType)], Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash p}{\Gamma\theta \vdash p\theta}\;\textsf{INST\_TYPE}$$

当 theta 两次给出同一个变量，或映射到状态不接纳的类型时，以 InvalidInstantiation 失败；当被实例化的常量不再是其模式的实例时，以 TypeMismatch 失败。

inst_checked

inst_checked(state, sigma, th) 是 INST：它在整个定理中同时用项代换自由变量。

pub fn inst_checked(KernelState, Array[(Term, Term)], Thm) -> Result[Thm, LogicError]

$$\frac{\Gamma \vdash p}{\Gamma\sigma \vdash p\sigma}\;\textsf{INST} \qquad \sigma = [x_1 \mapsto t_1, \dots, x_n \mapsto t_n],\; x_i, t_i : \tau_i$$

与 ABS 不同，INST 可以触及出现在假设中的变量，因为它也在假设中做代换。当键不是变量或重复出现时，以 InvalidInstantiation 失败；当值的类型与其键不同时，以 TypeMismatch 失败。

test "primitive rules" {
  let st = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let p = @kernel.mk_var("p", bool)
  let q = @kernel.mk_var("q", bool)
  // {p} |- p
  let th_p = @kernel.assume_checked(st, p).unwrap()
  inspect(@kernel.thm_to_string(th_p), content="[FVar(p : bool)] |- FVar(p : bool)")
  // {p = q} |- p = q, then EQ_MP gives {p = q, p} |- q
  let th_eq = @kernel.assume_checked(st, @kernel.mk_eq(p, q).unwrap()).unwrap()
  let th_q = @kernel.eq_mp_checked(st, th_eq, th_p).unwrap()
  inspect(@kernel.thm_hyp_count(th_q), content="2")
  inspect(@kernel.term_to_string(@kernel.thm_concl(th_q).unwrap()), content="Var(q : bool)")
  // DEDUCT_ANTISYM on {p} |- p and {q} |- q gives {p, q} |- p = q
  let th_q0 = @kernel.assume_checked(st, q).unwrap()
  let th_pq = @kernel.deduct_antisym_rule_checked(st, th_p, th_q0).unwrap()
  inspect(@kernel.thm_hyp_count(th_pq), content="2")
  // INST renames p to q everywhere
  let th_inst = @kernel.inst_checked(st, [(p, q)], th_p).unwrap()
  inspect(@kernel.thm_to_string(th_inst), content="[FVar(q : bool)] |- FVar(q : bool)")
  // ASSUME needs a proposition
  let x = @kernel.mk_var("x", @kernel.mk_tyvar("A"))
  inspect(@kernel.assume_checked(st, x) is Err(@kernel.NotBoolTerm), content="true")
}

test "equality rules" {
  let st = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let x = @kernel.mk_var("x", a)
  let y = @kernel.mk_var("y", a)
  let id = @kernel.mk_abs(x, x)
  // BETA: |- (λx. x) y = y
  let th_beta = @kernel.beta_rule_checked(st, @kernel.mk_comb(id, y)).unwrap()
  let (_, rhs) = @kernel.dest_eq(@kernel.thm_concl(th_beta).unwrap()).unwrap()
  inspect(@kernel.term_to_string(rhs), content="Var(y : A)")
  // TRANS with REFL on the right-hand side changes nothing
  let th_t = @kernel.trans_checked(st, th_beta, @kernel.refl_checked(st, y).unwrap()).unwrap()
  inspect(@kernel.thm_to_string(th_t) == @kernel.thm_to_string(th_beta), content="true")
  // ABS over y is refused: y is free in the hypothesis {x = y}
  let th_h = @kernel.assume_checked(st, @kernel.mk_eq(x, y).unwrap()).unwrap()
  inspect(@kernel.abs_rule_checked(st, y, th_h) is Err(@kernel.VarFreeInHyp), content="true")
  // INST_TYPE: instantiate A := bool
  let th_b = @kernel.inst_type(st, [("A", @kernel.bool_ty())], th_beta).unwrap()
  assert_eq(@kernel.term_tyvars(@kernel.thm_concl(th_b).unwrap()), [])
  // BETA needs a redex
  inspect(@kernel.beta_rule_checked(st, y) is Err(@kernel.NotTrivialBetaRedex), content="true")
}

内核状态

KernelState

KernelState 是抽象的逻辑状态：带作用域的常量签名，加上理论历史（定义、类型定义、规约、无穷锚点和审计证书）。

type KernelState

状态是不可变值。每个扩张状态的操作都返回新状态，旧状态仍然有效，因此可以保留较早的状态作为保守性检查的基础。

empty_kernel_state

empty_kernel_state 返回初始状态。

pub fn empty_kernel_state() -> KernelState

它声明一个常量，即标识为 0、模式为 $(\alpha \to \mathit{bool}) \to \alpha$ 的选择算子 @，并接纳类型 bool、ind 和 fun。等号常量 = 是内置的，无需声明；= 和 @ 是保留名称。

ks_add_const

ks_add_const(state, name, ty) 在最内层作用域中声明模式为 ty 的常量，并赋予它新的标识。

pub fn ks_add_const(KernelState, String, HolType) -> Result[KernelState, SigError]

在同一作用域中再次以相同类型声明同名常量，则状态保持不变。失败情形：该名称已在最内层作用域中以另一类型声明时为 ConstTypeConflict，对 = 和 @ 为 ReservedSymbol，对已定义的常量为 DefinitionAlreadyExists，名称被某个类型定义占用时为 TypeRepresentationAlreadyExists 或 TypeAbstractionAlreadyExists，ty 提到状态不接纳的类型时为 TypeMismatch。

ks_lookup_const、ks_const_schema 和 ks_lookup_const_id

ks_lookup_const 和 ks_const_schema 都返回某名称下可见常量所声明的模式；ks_lookup_const_id 返回其标识。最内层的声明优先。

pub fn ks_lookup_const(KernelState, String) -> HolType?
pub fn ks_const_schema(KernelState, String) -> HolType?
pub fn ks_lookup_const_id(KernelState, String) -> Int?

ks_mk_const 和 ks_mk_const_instance

ks_mk_const 构造可见常量在其模式类型上的一次出现，并记录其标识。ks_mk_const_instance 构造在模式的某个实例上的一次出现。

pub fn ks_mk_const(KernelState, String) -> Result[Term, SigError]
pub fn ks_mk_const_instance(KernelState, String, HolType) -> Result[Term, SigError]

当没有常量具有该名称时，两者都以 UnknownConst 失败。当类型不是模式的实例时，ks_mk_const_instance 以 InvalidConstInstance 失败；当类型不可容许时，以 TypeMismatch 失败。

ks_push_scope 和 ks_pop_scope

ks_push_scope 打开新的最内层作用域；ks_pop_scope 丢弃它以及其中声明的每个常量。

pub fn ks_push_scope(KernelState) -> KernelState
pub fn ks_pop_scope(KernelState) -> Result[KernelState, SigError]

在内层作用域中声明的常量会遮蔽外层同名常量，并获得新的标识。弹出只改变签名：作用域内记录的定义、类型定义和证书仍保留在理论历史中，因此它们的名称仍被占用。在最外层作用域上，ks_pop_scope 以 ScopeUnderflow 失败。

ks_sig

ks_sig 返回状态的签名部分。

pub fn ks_sig(KernelState) -> GlobalSig

ks_type_is_admissible 和 ks_type_subst_is_admissible

当类型中的每个类型构造子都是内置的，或已由类型定义接纳且元数正确时，ks_type_is_admissible 成立。当代换中的每个类型都可容许时，ks_type_subst_is_admissible 成立。

pub fn ks_type_is_admissible(KernelState, HolType) -> Bool
pub fn ks_type_subst_is_admissible(KernelState, Array[(String, HolType)]) -> Bool

ks_term_in_language 和 ks_thm_is_sentence_in_language

当项中的每个类型都可容许，且每个常量出现都是在其模式某个实例上的已声明常量（若记录了标识则标识须匹配）时，ks_term_in_language 成立。当定理没有假设且其结论是该状态语言中的闭命题时，ks_thm_is_sentence_in_language 成立。

pub fn ks_term_in_language(KernelState, Term) -> Bool
pub fn ks_thm_is_sentence_in_language(KernelState, Thm) -> Bool

test "scopes and constants" {
  let st0 = @kernel.empty_kernel_state()
  let a = @kernel.mk_tyvar("A")
  let st1 = @kernel.ks_add_const(st0, "c", a).unwrap()
  inspect(@kernel.term_to_string(@kernel.ks_mk_const(st1, "c").unwrap()), content="Const(c#1 : A)")
  let c_bool = @kernel.ks_mk_const_instance(st1, "c", @kernel.bool_ty()).unwrap()
  inspect(@kernel.term_to_string(c_bool), content="Const(c#1 : bool)")
  let th = @kernel.refl_checked(st1, @kernel.ks_mk_const(st1, "c").unwrap()).unwrap()
  // shadow c in an inner scope: the old theorem is no longer admissible there
  let st2 = @kernel.ks_add_const(@kernel.ks_push_scope(st1), "c", @kernel.bool_ty()).unwrap()
  assert_eq(@kernel.ks_lookup_const_id(st2, "c"), Some(2))
  inspect(@kernel.thm_is_admissible(st2, th), content="false")
  // pop the scope: the outer c is visible again and the theorem is usable
  let st3 = @kernel.ks_pop_scope(st2).unwrap()
  assert_eq(@kernel.ks_lookup_const_id(st3, "c"), Some(1))
  inspect(@kernel.thm_is_admissible(st3, th), content="true")
  inspect(@kernel.ks_pop_scope(st3) is Err(@kernel.ScopeUnderflow), content="true")
  inspect(@kernel.ks_add_const(st0, "@", a) is Err(@kernel.ReservedSymbol), content="true")
}

签名

GlobalSig 单独就是带作用域的常量表，不含理论历史。这些函数直接作用于它；它们从不产生 Thm。

GlobalSig 和 ConstId

GlobalSig 是作用域的栈，最内层在最后；每个作用域列出名称、标识和模式。ConstId 是已声明常量的整数标识。

pub enum GlobalSig {
  Sig(Array[Array[(String, Int, HolType)]])
}

pub type ConstId = Int

empty_sig、sig_push_scope 和 sig_pop_scope_e

empty_sig 是带有一个空作用域的签名；与 empty_kernel_state 的签名不同，它不包含 @。sig_push_scope 和 sig_pop_scope_e 打开和关闭作用域；弹出最后一个作用域会以 ScopeUnderflow 失败。

pub fn empty_sig() -> GlobalSig
pub fn sig_push_scope(GlobalSig) -> GlobalSig
pub fn sig_pop_scope_e(GlobalSig) -> Result[GlobalSig, SigError]

sig_has_const、sig_lookup_const 和 sig_lookup_const_id

这些函数从最内层作用域向外查找名称。

pub fn sig_has_const(GlobalSig, String) -> Bool
pub fn sig_lookup_const(GlobalSig, String) -> HolType?
pub fn sig_lookup_const_id(GlobalSig, String) -> Int?

sig_add_const_idempotent_e

sig_add_const_idempotent_e 在最内层作用域中以下一个空闲标识声明常量；若相同的声明已存在，则原样返回签名。

pub fn sig_add_const_idempotent_e(GlobalSig, String, HolType) -> Result[GlobalSig, SigError]

对 = 和 @ 以 ReservedSymbol 失败；当最内层作用域以另一类型声明了该名称时，以 ConstTypeConflict 失败。

sig_mk_const_e 和 sig_mk_const_instance_e

这些函数从签名构造常量出现，与 ks_mk_const 和 ks_mk_const_instance 类似，但不做内核状态那样的类型可容许性检查。

pub fn sig_mk_const_e(GlobalSig, String) -> Result[Term, SigError]
pub fn sig_mk_const_instance_e(GlobalSig, String, HolType) -> Result[Term, SigError]

sig_define_const_e

sig_define_const_e(sig, name, rhs) 在 rhs 的类型上声明 name，并以项的形式返回定义等式 $\mathit{name} = \mathit{rhs}$。

pub fn sig_define_const_e(GlobalSig, String, Term) -> Result[(GlobalSig, Term), SigError]

该等式只是一个项，而不是定理：此函数没有逻辑权威。要获得定义定理，请使用 ks_define_const_thm。当 rhs 类型错误时，以 InvalidConstRhs 失败。

扩张闸门

理论只通过三个闸门增长。每个闸门检查其附带条件，在理论历史中记录新名称，并追加一份审计证书。

ks_define_const 和 ks_define_const_thm

ks_define_const(state, c, ty, rhs) 是定义闸门 DefOK：它声明常量 c : ty 并记录定义 $c = \mathit{rhs}$。ks_define_const_thm 做同样的事并返回定义定理 $\vdash c = \mathit{rhs}$；ks_define_const 则以项的形式返回该等式。

pub fn ks_define_const(KernelState, String, HolType, Term) -> Result[(KernelState, Term), SigError]
pub fn ks_define_const_thm(KernelState, String, HolType, Term) -> Result[(KernelState, Thm), SigError]

附带条件为：c 不是保留名称，也未被定义或类型定义占用（ReservedSymbol、DefinitionAlreadyExists、TypeRepresentationAlreadyExists、TypeAbstractionAlreadyExists）；rhs 是闭项（DefinitionNotClosed）；rhs 不直接或通过更早的定义间接提到 c（DefinitionIsCyclic）；ty 可容许（InvalidConstRhs）且等于 rhs 的类型（TypeMismatch）；rhs 的每个类型变量都出现在 ty 中（GhostTypeVariable）；rhs 的每个常量都以其模式的某个实例声明（InvalidConstRhs）。内核设计说明说明了为何每个条件对保守性都是必需的。

ks_definition_theorem 和 ks_has_def_head

ks_definition_theorem 返回已定义常量所记录的定义定理，否则返回 Err(UnknownConst)。ks_has_def_head 测试某个名称是否已被定义。

pub fn ks_definition_theorem(KernelState, String) -> Result[Thm, SigError]
pub fn ks_has_def_head(KernelState, String) -> Bool

ks_register_type_definition

ks_register_type_definition(state, tycon, params, rep, pred, witness) 是类型定义闸门 TypeDefOK：它接纳元数为 params.length() 的新类型构造子 tycon，使其与表示类型中由 pred 划出的子集一一对应。

pub fn ks_register_type_definition(KernelState, String, Array[String], String, Term, Thm) -> Result[KernelState, SigError]

pred 必须是闭抽象 $\lambda (x{:}\rho).\,P$，其中 $P : \mathit{bool}$，且其类型变量都在 params 之中；witness 必须是无假设的定理 $\vdash P[w/x]$（w 为闭项），以表明该子集非空。成功时，状态声明 rep : tycon(params) -> ρ 和 Abs_<tycon> : ρ -> tycon(params)，并记录 ks_typedef_contract 返回的契约定理。失败会指出被违反的条件：InvalidTypeParams、InvalidTypeArity、InvalidTypeRepName、InvalidTypeAbsName、TypeConstructorAlreadyExists、TypeRepresentationAlreadyExists、TypeAbstractionAlreadyExists、InvalidTypePredicate、TypeWitnessArityMismatch、InvalidTypeWitness、TypeWitnessPredicateMismatch、InvalidTypeDefinitionProduct。

ks_typedef_contract 和 ks_has_typedef_contract

ks_typedef_contract(state, tycon) 返回类型定义的三条契约定理，否则返回 Err(MissingTypeDefinitionContract)。ks_has_typedef_contract 测试是否存在这样的契约。

pub fn ks_typedef_contract(KernelState, String) -> Result[(Thm, Thm, Thm), SigError]
pub fn ks_has_typedef_contract(KernelState, String) -> Bool

记 $\mathit{abs} = \texttt{Abs\_}\mathit{tycon}$，这三条定理依次为：

$$\vdash \mathit{abs}(\mathit{rep}\,a) = a \qquad \vdash P[\mathit{rep}\,a / x] \qquad P[r/x] \vdash \mathit{rep}(\mathit{abs}\,r) = r$$

ks_has_type_witness、ks_has_type_rep_head 和 ks_has_type_abs_head

ks_has_type_witness(state, tycon, arity) 测试该元数的类型构造子是否已被接纳；ind 从一开始就被接纳。另外两个函数测试某个名称是否是某个类型定义的表示函数或抽象函数。

pub fn ks_has_type_witness(KernelState, String, Int) -> Bool
pub fn ks_has_type_rep_head(KernelState, String) -> Bool
pub fn ks_has_type_abs_head(KernelState, String) -> Bool

ks_specify_const

ks_specify_const(state, c, ty, pred, witness) 是规约闸门 SpecOK：给定 $\vdash P[w/x]$，它引入常量 c : ty 并返回 $\vdash P[c/x]$。

pub fn ks_specify_const(KernelState, String, HolType, Term, Thm) -> Result[(KernelState, Thm), SigError]

该闸门由选择算子和 DefOK 导出：它通过 ks_define_const_thm 定义 $c = (@\,\mathit{pred})$，因此状态依次记录一份 DefOK 证书和一份 SpecOK 证书。pred 必须是 ty 上的闭抽象，且不含 ty 之外的类型变量（InvalidSpecificationPredicate、SpecificationTypeVarLeak），witness 必须是该谓词在某个闭项处的无假设定理（InvalidSpecificationWitness）。ks_define_const 的定义条件同样适用于 c。

ks_register_ind_infinity_axiom、ks_ind_infinity_axiom 和 ks_has_ind_infinity_axiom

ks_register_ind_infinity_axiom(state, anchor) 把一条关于 ind 的定理记录为该理论的无穷锚点。ks_ind_infinity_axiom 返回它，否则返回 Err(MissingInfinityAnchor)；ks_has_ind_infinity_axiom 测试是否已记录。

pub fn ks_register_ind_infinity_axiom(KernelState, Thm) -> Result[KernelState, SigError]
pub fn ks_ind_infinity_axiom(KernelState) -> Result[Thm, SigError]
pub fn ks_has_ind_infinity_axiom(KernelState) -> Bool

锚点必须已经是一个 Thm：无假设、可容许且提到 ind 的命题。因此注册不会增加新定理；它只是标明哪条定理扮演无穷假设的角色。当锚点已被记录，或该定理不合格时，以 InvalidInfinityAnchor 失败。

test "definitions" {
  let st = @kernel.empty_kernel_state()
  let bool = @kernel.bool_ty()
  let x = @kernel.mk_var("x", bool)
  let bb = @kernel.fun_ty(bool, bool)
  let (st1, def_th) = @kernel.ks_define_const_thm(st, "idb", bb, @kernel.mk_abs(x, x)).unwrap()
  inspect(
    @kernel.thm_to_string(def_th),
    content="[] |- Comb(Comb(Const(= : fun(fun(bool, bool), fun(fun(bool, bool), bool))), Const(idb#1 : fun(bool, bool))), Abs(bool. BVar(0 : bool)))",
  )
  inspect(@kernel.ks_has_def_head(st1, "idb"), content="true")
  // a name can be defined only once, and a definition must be closed
  inspect(
    @kernel.ks_define_const(st1, "idb", bb, @kernel.mk_abs(x, x)) is Err(@kernel.DefinitionAlreadyExists),
    content="true",
  )
  inspect(@kernel.ks_define_const(st, "k", bool, x) is Err(@kernel.DefinitionNotClosed), content="true")
  // λy. y = λy. y mentions the type variable B, which the type bool does not
  let y = @kernel.mk_var("y", @kernel.mk_tyvar("B"))
  let ghost = @kernel.mk_eq(@kernel.mk_abs(y, y), @kernel.mk_abs(y, y)).unwrap()
  inspect(@kernel.ks_define_const(st, "g", bool, ghost) is Err(@kernel.GhostTypeVariable), content="true")
}

test "specification" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "t0", bool).unwrap()
  let t0 = @kernel.ks_mk_const(st0, "t0").unwrap()
  let x = @kernel.mk_var("x", bool)
  let pred = @kernel.mk_abs(x, @kernel.mk_eq(x, t0).unwrap()) // λx. x = t0
  let witness = @kernel.refl_checked(st0, t0).unwrap() // |- t0 = t0
  let (st1, th) = @kernel.ks_specify_const(st0, "c", bool, pred, witness).unwrap()
  inspect(
    @kernel.thm_to_string(th),
    content="[] |- Comb(Comb(Const(= : fun(bool, fun(bool, bool))), Const(c#2 : bool)), Const(t0#1 : bool))",
  )
  inspect(@kernel.ks_extension_cert_count(st1), content="2")
}

test "type definition" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.ks_add_const(@kernel.empty_kernel_state(), "t0", bool).unwrap()
  let b = @kernel.mk_var("b", bool)
  let pred = @kernel.mk_abs(b, @kernel.mk_eq(b, b).unwrap()) // every bool
  let t0 = @kernel.ks_mk_const(st0, "t0").unwrap()
  let witness = @kernel.refl_checked(st0, t0).unwrap() // |- t0 = t0
  let st1 = @kernel.ks_register_type_definition(st0, "copy", [], "rep_copy", pred, witness).unwrap()
  inspect(@kernel.ks_type_is_admissible(st1, @kernel.mk_tyapp("copy", [])), content="true")
  assert_eq(
    @kernel.ks_lookup_const(st1, "Abs_copy").map(@kernel.hol_type_to_string),
    Some("fun(bool, copy)"),
  )
  let (abs_rep, _, _) = @kernel.ks_typedef_contract(st1, "copy").unwrap()
  inspect(
    @kernel.term_to_string(@kernel.thm_concl(abs_rep).unwrap()),
    content="Comb(Comb(Const(= : fun(copy, fun(copy, bool))), Comb(Const(Abs_copy : fun(bool, copy)), Comb(Const(rep_copy : fun(copy, bool)), Var(a : copy)))), Var(a : copy))",
  )
}

审计与重放

ExtensionGate 与 ExtensionCert

ExtensionGate 标明准许某次扩张的闸门。ExtensionCert 是一次准许的审计记录：包含闸门、它引入的名字，以及见证定理或定义定理的摘要。

pub enum ExtensionGate {
  DefOK
  TypeDefOK
  SpecOK
}

pub type ExtensionCert = (ExtensionGate, Array[String], String)

ks_extension_cert_count 与 ks_extension_cert_at

这些函数按准许顺序读取状态中的证书。

pub fn ks_extension_cert_count(KernelState) -> Int
pub fn ks_extension_cert_at(KernelState, Int) -> (ExtensionGate, Array[String], String)?

证书只记录发生过的事；它们不是证明对象，也不能转化为定理。

ks_conservative_replay_ok

ks_conservative_replay_ok(base, extended, th) 是可执行的保守性检查：当 th 在 extended 中可容许、是 base 语言中封闭且无假设的语句、并且在 base 中可容许时，该检查成立。

pub fn ks_conservative_replay_ok(KernelState, KernelState, Thm) -> Bool

回归测试用它检查：在扩张之后证明、但用旧语言陈述的定理，仍然是旧理论的定理。

test "audit" {
  let bool = @kernel.bool_ty()
  let st0 = @kernel.empty_kernel_state()
  let x = @kernel.mk_var("x", bool)
  let id = @kernel.mk_abs(x, x)
  let (st1, _) = @kernel.ks_define_const_thm(st0, "idb", @kernel.fun_ty(bool, bool), id).unwrap()
  inspect(@kernel.ks_extension_cert_count(st1), content="1")
  let (gate, heads, _) = @kernel.ks_extension_cert_at(st1, 0).unwrap()
  inspect(gate is @kernel.DefOK && heads == ["idb"], content="true")
  // |- (λx. x) = (λx. x) does not mention idb: it replays in the base theory
  let th = @kernel.refl_checked(st1, id).unwrap()
  inspect(@kernel.ks_conservative_replay_ok(st0, st1, th), content="true")
}

错误

LogicError

LogicError 由项构造函数和原始规则以值的形式抛出。

pub suberror LogicError {
  TypeMismatch
  VariableCaptured
  NotAnEquality
  NotBoolTerm
  AlphaMismatch
  InvalidInstantiation
  VarFreeInHyp
  NotTrivialBetaRedex
  BoundaryFailure
  CapacityExceeded
}

构造子	含义
TypeMismatch	某个项类型不良，应当一致的类型不一致，或者某个常量在该状态中未知。
VariableCaptured	代换值是一个松散的绑定索引。由具名项构造的值绝不会如此。
NotAnEquality	应当是等式的前提或项并不是等式。
NotBoolTerm	应当是命题的项具有其他类型。
AlphaMismatch	应当 α 等价的项并不等价。
InvalidInstantiation	代换格式错误，ABS 的绑定子不是变量，或者定理与该状态的常量标识不符。
VarFreeInHyp	ABS 变量在某个假设中自由出现。
NotTrivialBetaRedex	BETA 收到的项不是 β-redex。
BoundaryFailure	项无法在具名形式与 De Bruijn 形式之间转换。
CapacityExceeded	De Bruijn 索引的计算会发生溢出。

SigError

SigError 由签名操作和扩张闸门以值的形式抛出。

pub suberror SigError {
  DuplicateConstName
  ConstTypeConflict
  InvalidConstInstance
  UnknownConst
  ScopeUnderflow
  InvalidConstRhs
  ReservedSymbol
  DefinitionAlreadyExists
  DefinitionNotClosed
  DefinitionIsCyclic
  GhostTypeVariable
  InvalidTypeWitness
  InvalidTypePredicate
  InvalidTypeRepName
  InvalidTypeAbsName
  InvalidTypeParams
  InvalidTypeArity
  TypeWitnessArityMismatch
  TypeWitnessPredicateMismatch
  TypeConstructorAlreadyExists
  TypeRepresentationAlreadyExists
  TypeAbstractionAlreadyExists
  InvalidInfinityAnchor
  MissingInfinityAnchor
  InvalidTypeDefinitionProduct
  MissingTypeDefinitionContract
  InvalidSpecificationWitness
  InvalidSpecificationPredicate
  SpecificationTypeVarLeak
  TypeMismatch
}

分组	构造函数
签名	DuplicateConstName, ConstTypeConflict, InvalidConstInstance, UnknownConst, ScopeUnderflow, ReservedSymbol, TypeMismatch
DefOK	InvalidConstRhs, DefinitionAlreadyExists, DefinitionNotClosed, DefinitionIsCyclic, GhostTypeVariable
TypeDefOK	InvalidTypeWitness, InvalidTypePredicate, InvalidTypeRepName, InvalidTypeAbsName, InvalidTypeParams, InvalidTypeArity, TypeWitnessArityMismatch, TypeWitnessPredicateMismatch, TypeConstructorAlreadyExists, TypeRepresentationAlreadyExists, TypeAbstractionAlreadyExists, InvalidTypeDefinitionProduct, MissingTypeDefinitionContract
SpecOK	InvalidSpecificationWitness, InvalidSpecificationPredicate, SpecificationTypeVarLeak
无穷锚点	InvalidInfinityAnchor, MissingInfinityAnchor

两种错误类型都是值：用 is 或 match 匹配它们，如本页示例所示。