From 02a0f87be944b1d43fda265058b891f419d25b65 Mon Sep 17 00:00:00 2001 From: Chloe Brown Date: Tue, 16 Mar 2021 18:45:27 +0000 Subject: Change Language definition to respects instead of custom congruence. --- 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 4623066..754d92d 100644 --- a/src/Cfe/Judgement/Base.agda +++ b/src/Cfe/Judgement/Base.agda @@ -28,10 +28,10 @@ data _,_⊢_∶_ : {m : ℕ} → {n : ℕ} → Vec (Type ℓ ℓ) m → Vec (Typ Vee : ∀ {m n} {Γ : Vec _ m} {Δ : Vec _ n} {e₁ e₂ τ₁ τ₂} → Γ , Δ ⊢ e₁ ∶ τ₁ → Γ , Δ ⊢ e₂ ∶ τ₂ → (τ₁#τ₂ : τ₁ # τ₂) → Γ , Δ ⊢ e₁ ∨ e₂ ∶ τ₁ ∨ₜ τ₂ vcast : ∀ {a A m n} → .(m ≡ n) → Vec {a} A m → Vec A n +vcast {n = ℕ.zero} eq [] = [] vcast {n = suc n} eq (x ∷ xs) = x ∷ vcast (suc-injective eq) xs where open import Data.Nat.Properties using (suc-injective) -vcast {n = ℕ.zero} eq [] = [] data _≅_ {a A} : {m n : ℕ} → Vec {a} A m → Vec A n → Set a where []≅[] : [] ≅ [] -- cgit v1.2.3