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' 式はポイントフリー