diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-16 18:45:27 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-03-16 18:45:27 +0000 |
| commit | 02a0f87be944b1d43fda265058b891f419d25b65 (patch) | |
| tree | a6b289f1055dfa26efe276c503851db785d47f98 /src/Cfe/Judgement/Base.agda | |
| parent | 26925a4f41ed14881846648bf43448d07f1873d7 (diff) | |
Change Language definition to respects instead of custom congruence.
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 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 []≅[] : [] ≅ [] |