stella

stella 是一个用 MoonBit 编写、仍在开发中的证明助手。其内核是 elab 包：包含 Martin-Löf 类型论的核心语法、求值为值、读回为范式，以及一个双向类型检查器，其定义等价由求值归一化判定。

该类型论包含单位类型、 $\Pi$ 类型、 $\Sigma$ 类型、带 $J$ 消去子的恒等类型、带递归的 W 类型，以及直谓宇宙的累积层级，其子类型关系在 $\Pi$ 类型的定义域上逆变。

包

包	内容	API	教程	设计
`elab` (`src/elab`)	项（`TermInf`、`TermChk`、`Name`）、值（`Value`、`Neutral`）、求值与读回（`eval_inf`、`eval_chk`、`quote`）、类型检查（`type_inf`、`type_chk`、`type_inf_0`、`def_eq`、`TypeError`）。	API	教程	设计

该包还包含白盒测试（elaboration_wbtest.mbt），覆盖宇宙层级、子类型以及标注的类型规则。

初次接触依值类型。 阅读下面的论著直到 $\lambda\Pi$ 演算一章，然后跟着教程操作，它将恒等函数、对以及一个路径归纳证明构建为 MoonBit 值。
使用内核。 教程展示如何声明常量、检查项并将其归一化；API 参考说明每个函数的契约，包括何时抛出 TypeError、何时 panic。
开发内核。 设计说明以推理规则记法给出每条类型规则、求值与读回的方程、检查器所依赖的不变式，以及实现与理论之间的已知缺口。

stella 需要 moonc 0.10 或更新版本的 MoonBit，除 MoonBit 核心库外没有其他依赖。

moon add Luna-Flow/stella@0.1.2

import {
  "Luna-Flow/stella/elab",
  "moonbitlang/core/list",
}

在提交拉取请求前，请运行 moon check --target all 和 moon test。

下面的论述从无类型 lambda 演算一路发展到 Martin-Löf 类型论，阐述 stella 背后的类型理论，并说明内核如何对其进行 elaboration。在深入 elaboration 细节或扩展证明语言之前，请先把它当作整体概述来阅读。