カーネルの型付け規則（概略）

定義 2.1（「証明支援系 Lean の仕組み」§2）

文脈 $\Gamma$ と環境（登録済みの定数と、その型・定義）のもとで、

$\Gamma\vdash\mathsf{Sort}\ u:\mathsf{Sort}\ (u+1)$ 。
$\Gamma\vdash A:\mathsf{Sort}\ u$ かつ $\Gamma,x{:}A\vdash B:\mathsf{Sort}\ v$ ならば $\Gamma\vdash(x:A)\to B:\mathsf{Sort}\ (\mathrm{imax}\ u\ v)$ 。ここで $\mathrm{imax}\ u\ 0=0$ 、 $v\ne0$ なら $\mathrm{imax}\ u\ v=\max(u,v)$ 。
$\Gamma,x{:}A\vdash b:B$ ならば $\Gamma\vdash(\mathsf{fun}\ x:A\Rightarrow b):(x:A)\to B$ 。
$\Gamma\vdash f:(x:A)\to B$ 、 $\Gamma\vdash a:A'$ 、 $\Gamma\vdash A\equiv A'$ ならば $\Gamma\vdash f\,a:B[x:=a]$ 。
定数 $c$ は環境に登録された型をもつ（宇宙変数は具体化してよい）。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。

証明で明示的に参照している定理は、まだありません。