diff --git a/mambo.agda b/mambo.agda index 7dddb7b..1cd9f14 100644 --- a/mambo.agda +++ b/mambo.agda @@ -123,3 +123,4 @@ data _⊢_ : Context → Formula → Type where ¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥ □ₑ : Γ ⊢ □ X → X ∈ Δ → Γ ++ boxed Δ ⊢ Y □ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X + -- TODO: Maybe make it KT45