Introduce < for Languages.

Move around some definitions.

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