From 2cd74f160389fe2ab2b30ab628fbb9b712f06faf Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Tue, 28 Oct 2025 12:34:23 -0500
Subject: Split System into smaller modules

---
 Data/System/Values.agda | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 Data/System/Values.agda

(limited to 'Data/System')

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