From 0708355c7988345c98961cad087dc56eeb16ea7f Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 24 Apr 2021 15:30:30 +0100
Subject: Cleanup Derivation.

---
 src/Cfe/Derivation/Base.agda | 54 ++++++++++++++++++++++++--------------------
 1 file changed, 29 insertions(+), 25 deletions(-)

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

diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda
index ce368d0..0432c3d 100644
--- a/src/Cfe/Derivation/Base.agda
+++ b/src/Cfe/Derivation/Base.agda
@@ -8,37 +8,41 @@ module Cfe.Derivation.Base
 
 open Setoid over renaming (Carrier to C; _≈_ to _∼_)
 
-open import Cfe.Expression over hiding (_≋_)
-open import Data.Fin
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
+open import Cfe.Expression over hiding (_≈_)
+open import Data.Fin using (zero)
+open import Data.List using (List; []; [_]; _++_)
+open import Data.List.Relation.Binary.Equality.Setoid over using (_≋_)
 open import Level using (_⊔_)
 
 infix 5 _⤇_
 infix 4 _≈_
 
 data _⤇_ : Expression 0 → List C → Set (c ⊔ ℓ) where
-  Eps : ε ⤇ []
+  Eps  : ε ⤇ []
   Char : ∀ {c y} → (c∼y : c ∼ y) → Char c ⤇ [ y ]
-  Cat : ∀ {e₁ e₂ l₁ l₂ l} → e₁ ⤇ l₁ → e₂ ⤇ l₂ → l₁ ++ l₂ ≋ l → e₁ ∙ e₂ ⤇ l
-  Veeˡ : ∀ {e₁ e₂ l} → e₁ ⤇ l → e₁ ∨ e₂ ⤇ l
-  Veeʳ : ∀ {e₁ e₂ l} → e₂ ⤇ l → e₁ ∨ e₂ ⤇ l
-  Fix : ∀ {e l} → e [ μ e / zero ] ⤇ l → μ e ⤇ l
+  Cat  : ∀ {e₁ e₂ w₁ w₂ w} → e₁ ⤇ w₁ → e₂ ⤇ w₂ → w₁ ++ w₂ ≋ w → e₁ ∙ e₂ ⤇ w
+  Veeˡ : ∀ {e₁ e₂ w} → e₁ ⤇ w → e₁ ∨ e₂ ⤇ w
+  Veeʳ : ∀ {e₁ e₂ w} → e₂ ⤇ w → e₁ ∨ e₂ ⤇ w
+  Fix  : ∀ {e w} → e [ μ e / zero ] ⤇ w → μ e ⤇ w
 
-data _≈_ : ∀ {e l l′} → REL (e ⤇ l) (e ⤇ l′) (c ⊔ ℓ) where
-  Eps : Eps ≈ Eps
+data _≈_ : ∀ {e w w′} → REL (e ⤇ w) (e ⤇ w′) (c ⊔ ℓ) where
+  Eps  : Eps ≈ Eps
   Char : ∀ {c y y′} → (c∼y : c ∼ y) → (c∼y′ : c ∼ y′) → Char c∼y ≈ Char c∼y′
-  Cat : ∀ {e₁ e₂ l l₁ l₂ l₁′ l₂′ e₁⤇l₁ e₁⤇l₁′ e₂⤇l₂ e₂⤇l₂′} →
-          (e₁⤇l₁≈e₁⤇l′ : _≈_ {e₁} {l₁} {l₁′} e₁⤇l₁ e₁⤇l₁′) →
-          (e₂⤇l₂≈e₂⤇l′ : _≈_ {e₂} {l₂} {l₂′} e₂⤇l₂ e₂⤇l₂′) →
-          (eq : l₁ ++ l₂ ≋ l) → (eq′ : l₁′ ++ l₂′ ≋ l) →
-          Cat e₁⤇l₁ e₂⤇l₂ eq ≈ Cat e₁⤇l₁′ e₂⤇l₂′ eq′
-  Veeˡ : ∀ {e₁ e₂ l l′ e₁⤇l e₁⤇l′} →
-         (e₁⤇l≈e₁⤇l′ : _≈_ {e₁} {l} {l′} e₁⤇l e₁⤇l′) →
-         Veeˡ {e₂ = e₂} e₁⤇l ≈ Veeˡ e₁⤇l′
-  Veeʳ : ∀ {e₁ e₂ l l′ e₂⤇l e₂⤇l′} →
-         (e₂⤇l≈e₂⤇l′ : _≈_ {e₂} {l} {l′} e₂⤇l e₂⤇l′) →
-         Veeʳ {e₁} e₂⤇l ≈ Veeʳ e₂⤇l′
-  Fix : ∀ {e l l′ e[μe/0]⤇l e[μe/0]⤇l′} →
-        (e[μe/0]⤇l≈e[μe/0]⤇l′ : _≈_ {e [ μ e / zero ]} {l} {l′} e[μe/0]⤇l e[μe/0]⤇l′) →
-        Fix {e} e[μe/0]⤇l ≈ Fix e[μe/0]⤇l′
+  Cat  :
+    ∀ {e₁ e₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} →
+    (e₁⤇w₁≈e₁⤇w′ : _≈_ {e₁} {w₁} {w₁′} e₁⤇w₁ e₁⤇w₁′) →
+    (e₂⤇w₂≈e₂⤇w′ : _≈_ {e₂} {w₂} {w₂′} e₂⤇w₂ e₂⤇w₂′) →
+    (eq : w₁ ++ w₂ ≋ w) → (eq′ : w₁′ ++ w₂′ ≋ w) →
+    Cat e₁⤇w₁ e₂⤇w₂ eq ≈ Cat e₁⤇w₁′ e₂⤇w₂′ eq′
+  Veeˡ :
+    ∀ {e₁ e₂ w w′ e₁⤇w e₁⤇w′} →
+    (e₁⤇w≈e₁⤇w′ : _≈_ {e₁} {w} {w′} e₁⤇w e₁⤇w′) →
+    Veeˡ {e₂ = e₂} e₁⤇w ≈ Veeˡ e₁⤇w′
+  Veeʳ :
+    ∀ {e₁ e₂ w w′ e₂⤇w e₂⤇w′} →
+    (e₂⤇w≈e₂⤇w′ : _≈_ {e₂} {w} {w′} e₂⤇w e₂⤇w′) →
+    Veeʳ {e₁} e₂⤇w ≈ Veeʳ e₂⤇w′
+  Fix  :
+    ∀ {e w w′ e[μe/0]⤇w e[μe/0]⤇w′} →
+    (e[μe/0]⤇w≈e[μe/0]⤇w′ : _≈_ {e [ μ e / zero ]} {w} {w′} e[μe/0]⤇w e[μe/0]⤇w′) →
+    Fix {e} e[μe/0]⤇w ≈ Fix e[μe/0]⤇w′
-- 
cgit v1.2.3