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

Clean

Browse Source
This commit is contained in:
pingu
2025-12-30 10:45:04 +01:00
parent ed29a2d98b
commit f22c637eb0
1 changed files with 14 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files

28
mambo.agda
View File

@@ -185,20 +185,20 @@ inBoth {A} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ'
inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂) inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂)
weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A
weak {Δ} {Γ} {A} {Γ'} (var x) x₁ = var (x₁ x) weak (var x) x₁ = var (x₁ x)
weak {Δ} {Γ} {A} {Γ'} (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁) weak (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
weak {Δ} {Γ} {A} {Γ'} (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁) weak (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
weak {Δ} {Γ} {A} {Γ'} (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁) weak (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
weak {Δ} {Γ} {A} {Γ'} (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁) weak (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁) weak (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁) weak (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
weak {Δ} {Γ} {A} {Γ'} (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁)) weak (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
weak {Δ} {Γ} {A} {Γ'} (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁)) weak (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
weak {Δ} {Γ} {A} {Γ'} (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁)) weak (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
weak {Δ} {Γ} {A} {Γ'} (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁) weak (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
weak {Δ} {Γ} {A} {Γ'} (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁) weak (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
weak {Δ} {Γ} {A} {Γ'} (□ᵢ x) x₁ = □ᵢ x weak (□ᵢ x) x₁ = □ᵢ x
weak {Δ} {Γ} {A} {Γ'} (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁) weak (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A
weak-modal (var x) x₁ = var x weak-modal (var x) x₁ = var x