From da429008d25ac87ec67a4fb18a5cbee0ba756bcf Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Mon, 5 Apr 2021 14:31:57 +0100
Subject: Clean-up Language hierarchy.

---
 src/Cfe/Language/Construct/Single.agda | 27 ---------------------------
 1 file changed, 27 deletions(-)
 delete mode 100644 src/Cfe/Language/Construct/Single.agda

(limited to 'src/Cfe/Language/Construct/Single.agda')

diff --git a/src/Cfe/Language/Construct/Single.agda b/src/Cfe/Language/Construct/Single.agda
deleted file mode 100644
index ddea1a6..0000000
--- a/src/Cfe/Language/Construct/Single.agda
+++ /dev/null
@@ -1,27 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-
-open import Function
-open import Relation.Binary
-import Relation.Binary.PropositionalEquality as ≡
-
-module Cfe.Language.Construct.Single
-  {c ℓ} (over : Setoid c ℓ)
-  where
-
-open Setoid over renaming (Carrier to C)
-
-open import Cfe.Language over hiding (_≈_)
-open import Data.List
-open import Data.List.Relation.Binary.Equality.Setoid over
-open import Data.Product as Product
-open import Data.Unit
-open import Level
-
-｛_｝ : C → Language (c ⊔ ℓ)
-｛ c ｝ = record
-  { 𝕃 = [ c ] ≋_
-  ; ∈-resp-≋ = λ l₁≋l₂ l₁∈｛c｝ → ≋-trans l₁∈｛c｝ l₁≋l₂
-  }
-
-xy∉｛c｝ : ∀ c x y l → x ∷ y ∷ l ∉ ｛ c ｝
-xy∉｛c｝ c x y l (_ ∷ ())
-- 
cgit v1.2.3