MetaPRL 的修理告一段落了。在这篇文章里我来介紹一下它用起來大概是什么感觉的。

MetaPRL 不是像 Agda/Lean 那样直接写 proof script 然后 type check，也不是 HOL 那样完全在 repl 里做 interactive 操作，而是一半一半：proposition 先全写在文件里，编译成 rewrite abstract machine 后，link 到 Toplevel 程序，再用 repl 来进行 interactive proof，或者查阅，也可以 print 到 html 或 latex。

MetaPRL 中 proposition, tactic, inference rule 之间没有分別。primitive inference rule 就是不需要证明的 tactic，proposition 就是具有证明的 inference rule。因为用的是类似 sequent calculus 的 language，所以能定义表现力强于其它 proof assistant 里用 lemma 或 tactic 的 metatheorem。这一点原版的 NuPRL 也只是能自定义 inference rule 而不能给出 conservative extension 的证明。比如

显然易见，对形式为 $\Gamma, x:\mathbb{B}, \Delta[x] \vdash C[x]$ 的 goal 应用这个 tactic，就会生成 $\Gamma, \Delta[True] \vdash C[True]$ 和 $\Gamma, \Delta[False] \vdash C[False]$ 两个 goal。在 Agda 里这要用 dependent pattern match, 在 HOL 要用 primitive inference rule compose tactic，而在 MetaPRL 里这只是个能证明的 theorem，而且做为 tactic 没有 HOL tactic 必須要用 primitive inference rule 的 overhead。

这里的 unfold_btrue 等则是 inference 以外的另一种构造，rewrite rule

data definition 是不需证明的 rewrite rule，而且作为 NuPRL ITT 风格的 type theory，rewrite rule 是 pure computational 的，不需要 type check 就能应用。还是那个的经典的例子：

$\Gamma \vdash {\tt if}\ true\ {\tt then}\ 1\ {\tt else}\ ''what?'' \in \mathbb{Z}$

除了 ITT 以外，作为 meta logic framework, MetaPRL 还实现了 FOL, CZF, CIC。

其实它还有个 browser interface。