Split System into smaller modules

1 files changed, 21 insertions, 0 deletions

diff --git a/Data/System/Values.agda b/Data/System/Values.agda
new file mode 100644
index 0000000..bf8fa38
--- /dev/null
+++ b/Data/System/Values.agda
@@ -0,0 +1,21 @@
+{-# OPTIONS --without-K --safe #-}
+
+module Data.System.Values (A : Set) where
+
+open import Data.Nat.Base using (ℕ)
+open import Data.Vec.Functional using (Vector)
+open import Level using (0ℓ)
+open import Relation.Binary using (Rel; Setoid)
+open import Data.Vec.Functional.Relation.Binary.Equality.Setoid using (≋-setoid)
+
+import Relation.Binary.PropositionalEquality as ≡
+
+Values : ℕ → Setoid 0ℓ 0ℓ
+Values = ≋-setoid (≡.setoid A)
+
+_≋_ : {n : ℕ} → Rel (Vector A n) 0ℓ
+_≋_ {n} = Setoid._≈_ (Values n)
+
+infix 4 _≋_
+
+module ≋ {n : ℕ} = Setoid (Values n)