diff options
Diffstat (limited to 'src/Cfe/Language/Base.agda')
| -rw-r--r-- | src/Cfe/Language/Base.agda | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda index a3b5136..71ee7df 100644 --- a/src/Cfe/Language/Base.agda +++ b/src/Cfe/Language/Base.agda @@ -63,6 +63,13 @@ record _≈_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ f : ∀ {l} → l ∈ A → l ∈ B f⁻¹ : ∀ {l} → l ∈ B → l ∈ A +record _<_ {a b} (A : Language a) (B : Language b) : Set (c ⊔ ℓ ⊔ a ⊔ b) where + field + f : ∀ {l} → l ∈ A → l ∈ B + l : List C + l∉A : l ∉ A + l∈B : l ∈ B + null : ∀ {a} → Language a → Set a null A = [] ∈ A |