diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-12 17:32:33 +0100 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2021-04-12 17:32:33 +0100 |
| commit | 0dd077cd1f9d062bab43e1bfa4bd05e318ed09b2 (patch) | |
| tree | a3c2ae5af8268f51b96964332891ee7229bb9acf | |
| parent | f84e919e12c92c241d3d38203400c2bb14fb0017 (diff) | |
Remove unnecessary comment.
| -rw-r--r-- | src/Cfe/Type/Properties.agda | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda index 29fa287..21051c0 100644 --- a/src/Cfe/Type/Properties.agda +++ b/src/Cfe/Type/Properties.agda @@ -370,19 +370,6 @@ setoid {fℓ} {lℓ} = record { isEquivalence = ≈-isEquivalence {fℓ} {lℓ} step (s≤s m≤n) = mono (step m≤n) ------------------------------------------------------------------------ --- ⋃-⊨ : ∀ {a fℓ lℓ} {F : Op₁ (Language a)} {τ : Type fℓ lℓ} → --- (Congruent₁ _≤ˡ_ F) → --- (∀ {L} → L ⊨ τ → F L ⊨ τ) → ⋃ F ⊨ τ --- ⋃-⊨ {a} {F = F} {τ} ≤-mono ⊨-mono = record --- ; l⇒l = λ --- { (_ , l≢ε , (m , l∈Fᵐ) , _ , (n , l++x∷l′∈Fⁿ)) → --- _⊨_.l⇒l (Fⁿ⊨τ (m + n)) --- (-, l≢ε , _≤ˡ_.f (^-mono (≤-stepsʳ {m} n ≤ⁿ-refl)) l∈Fᵐ , --- -, _≤ˡ_.f (^-mono (≤-stepsˡ m ≤ⁿ-refl)) l++x∷l′∈Fⁿ) --- } --- } - ------------------------------------------------------------------------- -- Properties of _⊛_ ------------------------------------------------------------------------ |