diff options
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 (_ ∷ ()) |