blob: ddea1a649ef2e681a1675ed6463704cd93789ffc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
{-# OPTIONS --without-K --safe #-}
open import Function
open import Relation.Binary
import Relation.Binary.PropositionalEquality as ≡
module Cfe.Language.Construct.Single
{c ℓ} (over : Setoid c ℓ)
where
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 ⊔ ℓ)
｛ c ｝ = record
{ 𝕃 = [ 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 (_ ∷ ())
|
