混合コンテキストは、次を混ぜたもの。
- 型宣言文
- 値割り当て文
型宣言文だけのコンテキスト（実体は依存レコード＝テレスコープ）は指標〈signature〉。型宣言されたすべての名前に値割り当てしたコンテキストは環境〈environment〉と呼ぶ。
混合コンテキストは、指標と環境が混じったもの。混合コンテキストが非接地だとは、未宣言の名前がパターン変数として含まれるもの。しかし、混合コンテキストを環境と呼ぶこともある。
計算項の型チェック整合性〈consistency〉と、証明項の正当性〈correctness〉は同じ概念である。以下「≡」は定義等値〈definitionary equal〉。
- 整合性： inferType(Γ, aTerm) ≡ aType
- 正当性： inferType(Γ, aProof) ≡ aStatenamet
以上は、証明の検証系〈verifier〉の動作。Leanカーネルは検証系＝証明チェッカー＝型チェッカーになっている。項の型宣言（型と計算項）と定理（ステートメント命題と証明項）のチェッカーがカーネル機能＝チェッカー機能。
カーネル＝チェッカーへの入力構文をコア構文＝カーネル構文と呼ぶ。表層構文からコア構文への変換はエラボレーターが行う。
実際の実装がどうであれ、次のような略記と考えるとよい。
- theorem ＝ @[theorem] def 関数
- class ＝ @[class] structure 機能型
- instance ＝ @[instance] def 関数
- axiom ＝ @[axiom] decl 型宣言
- constant ＝ @[constant] decl 型宣言
宣言文には整合性の概念はない。ただし、整形式性〈well-defined-ness〉はある。割り当て文には整合性の概念があり、チェッカー＝検証系でチェックされる。
「関数」という概念と、関数定義文（名前に計算項の割り当て文）があるのと同様に、「定理＝ルール」という概念があり、定理定義文（名前に証明項の割り当て文）がある。関数定義のボディが計算項〈計算の記述構文〉、定理定義のボディが証明項〈証明の記述構文〉。
- 関数 ＝ 定理
- 計算 ＝ 証明
- 関数記述〈関数定義〉 ＝ 定理記述
- 関数名 ＝ 定理名
- 引数型 ＝ 前提命題
- 引数変数名 ＝ 前提命題ラベル
- 戻り値型 ＝ ターゲット命題
- 戻り値変数名 ＝ ターゲット命題ラベル
- 関数ボディの計算項〈computation term〉 ＝ 定理ボディの証明項〈proof term〉
- オラクル関数〈非計算的〉 ＝ オラクル定理〈非証明的〉
- 計算コンビネータ ＝ 証明コンビネータ〈リーズニング〉
- 基本関数 ＝ 推論規則〈証明規則〉
- 組み込み関数 ＝ 公理規則 ＝ 組み込み証明
- 関数の適用 ＝ 定理〈ルール〉の適用
- 関数の結合 ＝ 定理〈ルール〉の結合
- 型の要素〈無引数関数〉 ＝ 命題の保証〈無前提証明〉
- 関数要素 ＝ 含意命題の保証
- カリー同型 ＝ 演繹定理
- カリー変形 ＝ ゲンツェン変形
- 計算の環境 ＝ 証明の環境〈コンテキスト〉
- call 関数呼び出し ＝ use 定理呼び出し
- let x:X := this ＝ have p: A from this
