From 13e0839831a528d26478a3a94c7470204460cce4 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 29 Mar 2021 18:08:09 +0100
Subject: Introduce < for Languages.

Move around some definitions.
---
 src/Cfe/Language/Base.agda | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src/Cfe/Language/Base.agda')

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
 
-- 
cgit v1.2.3