From a92f724a46a78af74121c44bbb06c4ec51f9555e Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 23 Mar 2021 12:19:30 +0000 Subject: Replace transfer with shift. Prove substitution in the unguarded context. --- src/Cfe/Judgement/Base.agda | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/Cfe/Judgement/Base.agda') diff --git a/src/Cfe/Judgement/Base.agda b/src/Cfe/Judgement/Base.agda index 0e5417a..4be0256 100644 --- a/src/Cfe/Judgement/Base.agda +++ b/src/Cfe/Judgement/Base.agda @@ -21,7 +21,7 @@ data _⊢_∶_ : {n : ℕ} → Context n → Expression n → Type ℓ ℓ → S Eps : ∀ {n} {Γ,Δ : Context n} → Γ,Δ ⊢ ε ∶ Lift ℓ ℓ τε 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) + Var : ∀ {n} {Γ,Δ : Context n} {i} (i≥m : toℕ i ≥ _) → Γ,Δ ⊢ Var i ∶ lookup (Context.Γ Γ,Δ) (reduce≥′ (Context.m≤n Γ,Δ) i≥m) 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₂ ∶ τ₁ ∨ₜ τ₂ -- cgit v1.2.3