diff options
Diffstat (limited to 'src/Cfe')
| -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 _⊛_ ------------------------------------------------------------------------ |