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

Also have one example of K in it :D

Browse Source
This commit is contained in:
pingu
2025-12-25 14:04:20 +01:00
parent 45b888cc73
commit 1e949cb9ad
1 changed files with 7 additions and 2 deletions
Download Patch File Download Diff File Expand all files Collapse all files

9
mambo.agda
View File

@@ -84,6 +84,11 @@ ExampleModel .M.L 1 = 1 ∷ 2 ∷ []
ExampleModel .M.L 2 = 0 ∷ 2 ∷ [] ExampleModel .M.L 2 = 0 ∷ 2 ∷ []
ExampleModel .M.L _ = [] ExampleModel .M.L _ = []
KSem : ExampleModel , 0 ⊩ □ (atom 1 ⇒ atom 2) ⇒ (□ atom 1 ⇒ □ atom 2)
KSem x x₁ y zeroone = succ 2 (2 ∷ []) (zero 2 [])
KSem x x₁ y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
ExampleSem : ExampleModel , 0 ⊩ □ (atom 2) ExampleSem : ExampleModel , 0 ⊩ □ (atom 2)
ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 []) ExampleSem y zeroone = succ 2 (2 ∷ []) (zero 2 [])
ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 2 []) ExampleSem y zerotwo = succ 2 (2 ∷ []) (zero 2 [])
@@ -122,8 +127,8 @@ data _/_⊢_ (Δ Γ : Context) : Formula → Type where
□ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y □ₑ : Δ / Γ ⊢ □ X → (Δ , X) / Γ ⊢ Y → Δ / Γ ⊢ Y
-- TODO: Maybe make it KT45 -- TODO: Maybe make it KT45
K : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y) KSym : [] / [] ⊢ □ (X ⇒ Y) ⇒ (□ X ⇒ □ Y)
K {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y))))) KSym {X} {Y} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ X) ([] , (□ (X ⇒ Y)))))
(□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) []))) (□ₑ (var (succ (□(X ⇒ Y)) ([] , (□ (X ⇒ Y))) (zero (□ (X ⇒ Y)) [])))
(□ᵢ (mp (□ᵢ (mp
(var (zero (X ⇒ Y) ([] , X))) (var (zero (X ⇒ Y) ([] , X)))