diff options
| author | Chloe Brown <chloe.brown.00@outlook.com> | 2024-01-23 14:54:53 +0000 |
|---|---|---|
| committer | Chloe Brown <chloe.brown.00@outlook.com> | 2024-01-23 14:54:53 +0000 |
| commit | e7557267586b4c197663919ee83fa3e5c40e28f9 (patch) | |
| tree | f68f2fd8656e5b6ef153afed980c076a1209d56a /src/Cfe/Derivation/Base.agda | |
| parent | 06423f2a738b6ff94429ab84b4dcd3b443fd84bd (diff) | |
Diffstat (limited to 'src/Cfe/Derivation/Base.agda')
| -rw-r--r-- | src/Cfe/Derivation/Base.agda | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/Cfe/Derivation/Base.agda b/src/Cfe/Derivation/Base.agda index 0432c3d..373b6b5 100644 --- a/src/Cfe/Derivation/Base.agda +++ b/src/Cfe/Derivation/Base.agda @@ -13,6 +13,7 @@ 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 (_⊔_) +open import Relation.Binary.Core using (Rel) infix 5 _⤇_ infix 4 _≈_ @@ -29,10 +30,10 @@ 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₂ w w₁ w₂ w₁′ w₂′ e₁⤇w₁ e₁⤇w₁′ e₂⤇w₂ e₂⤇w₂′} → + ∀ {e₁ e₂ w 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) → + (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′} → |