diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-21 13:14:22 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-21 13:14:22 +0000 |
| commit | 9c72c8ed0c3e10b5dafb41e438285b08f244ba68 (patch) | |
| tree | 82def397b7d28635d6e1555fe58e2c45d13542f2 /src/Cfe/Judgement/Base.agda | |
| parent | 4e0ceac75e6d9940f0e11f93a3815448df258c70 (diff) | |
Prove judgement weakening.
Diffstat (limited to 'src/Cfe/Judgement/Base.agda')
| -rw-r--r-- | src/Cfe/Judgement/Base.agda | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda index 6b42598..0e5417a 100644 --- a/src/Cfe/Judgement/Base.agda +++ b/src/Cfe/Judgement/Base.agda @@ -22,6 +22,6 @@ data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → S Char : ∀ {n} {Γ,Δ : Context n} c → Γ,Δ ⊢ Char c ∶ Lift ℓ ℓ τ[ c ] Bot : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ⊥ ∶ Lift ℓ ℓ τ⊥ Var : ∀ {n} {Γ,Δ : Context n} {i} (i≥m : toℕ i ≥ _) → Γ,Δ ⊢ Var i ∶ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) i i≥m) - Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons τ Γ,Δ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ + Fix : ∀ {n} {Γ,Δ : Context n} {e τ} → cons Γ,Δ τ ⊢ e ∶ τ → Γ,Δ ⊢ μ e ∶ τ Cat : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → shift Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁⊛τ₂ : τ₁ ⊛ τ₂) → Γ,Δ ⊢ e₁ ∙ e₂ ∶ τ₁ ∙ₜ τ₂ Vee : ∀ {n} {Γ,Δ : Context n} {e₁ e₂ τ₁ τ₂} → Γ,Δ ⊢ e₁ ∶ τ₁ → Γ,Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ,Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂ |