pingu/mambo
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

Add new todo

Browse Source
This commit is contained in:
pingu
2025-12-22 21:31:51 +01:00
parent 411109a2ee
commit b322bac402
1 changed files with 1 additions and 0 deletions
Download Patch File Download Diff File Expand all files Collapse all files

1
mambo.agda
View File

@@ -123,3 +123,4 @@ data _⊢_ : Context → Formula → Type where
¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥ ¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥
□ₑ : Γ ⊢ □ X → X ∈ Δ → Γ ++ boxed Δ ⊢ Y □ₑ : Γ ⊢ □ X → X ∈ Δ → Γ ++ boxed Δ ⊢ Y
□ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X □ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X
-- TODO: Maybe make it KT45