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/Language/Construct/Single.agda | |
| parent | 26925a4f41ed14881846648bf43448d07f1873d7 (diff) | |
Change Language definition to respects instead of custom congruence.
Diffstat (limited to 'src/Cfe/Language/Construct/Single.agda')
| -rw-r--r-- | src/Cfe/Language/Construct/Single.agda | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda index b06be3d..ddea1a6 100644 --- a/src/Cfe/Language/Construct/Single.agda +++ b/src/Cfe/Language/Construct/Single.agda @@ -12,17 +12,16 @@ open Setoid over renaming (Carrier to C) open import Cfe.Language over hiding (_≈_) open import Data.List +open import Data.List.Relation.Binary.Equality.Setoid over open import Data.Product as Product open import Data.Unit open import Level -｛_｝ : C → Language (c ⊔ ℓ) 0ℓ +｛_｝ : C → Language (c ⊔ ℓ) ｛ c ｝ = record - { Carrier = λ l → ∃[ a ] (l ≡.≡ [ a ] × a ≈ c) - ; _≈_ = λ _ _ → ⊤ - ; isEquivalence = record - { refl = tt - ; sym = λ _ → tt - ; trans = λ _ _ → tt - } + { 𝕃 = [ c ] ≋_ + ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂ } + +xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝ +xy∉｛c｝ c x y l (_ ∷ ()) |