| Lean | ILean | 復CCC | 論理 |
|---|---|---|---|
| : | ⇒ | → | → |
| → | → | [,] | ⊃ |
| 空白 | :: | : | (なし) |
| ∧ | ∧ | × | ∧ |
| true | true | 1 | T |
| false | false | 0 | ⊥ |
| 空白区切り | 空白区切り | カンマ区切り | カンマ区切り |
| (なし) | (なし) | ストリング図 | 横棒図 |
| 命題 | 命題 | 対象 | 論理式 |
| 命題リスト | 命題リスト | 対象リスト | 論理式リスト |
| 証明項 | 証明項 | ポイント射 | N*証明 |
| ルール | ルール | 生成射 | N*推論規則 |
| タクティク | タクティク | オペレータ | L*推論規則 |
| 空白併置 | ◁ | rev | MP |
| (なし) | ▷ | lev | MP |
| (なし) | ; | ; | cut |
| (なし) | |
|
cut |
選言の例：
- Lean： f Γ : B
- ILean： f:: Γ ⇒ B
- 圏論： f:Γ' → B 環境はラベル無し環境
定義の例：
- Lean： f Γ : B := E または f' : B := λ Γ, E
- ILean： f:: Γ ⇒ B := E または f':: ⇒ B := λ Γ, E
- 圏論： f:Γ' → B := E' 式はポイントフリー
