From c4367035ec0638d5639157e98e6756d3779aeee5 Mon Sep 17 00:00:00 2001
From: Jacques Comeaux <jacquesrcomeaux@protonmail.com>
Date: Sat, 6 Dec 2025 16:40:13 -0600
Subject: Move FinMerge utilites

---
 FinMerge.agda            |  3 ++-
 FinMerge/Properties.agda |  3 ++-
 FinMerge/Util.agda       | 32 ++++++++++++++++++++++++++++++++
 Util.agda                | 32 --------------------------------
 4 files changed, 36 insertions(+), 34 deletions(-)
 create mode 100644 FinMerge/Util.agda
 delete mode 100644 Util.agda

diff --git a/FinMerge.agda b/FinMerge.agda
index d7b3f0b..2210e2f 100644
--- a/FinMerge.agda
+++ b/FinMerge.agda
@@ -13,8 +13,9 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-R
 open import Function using (id ; _∘_ ; _$_)
 open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe; map)
 
-open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
+open import FinMerge.Util using (_<_≤_; Ordering; compare)
 
+open Ordering
 
 private
   variable
diff --git a/FinMerge/Properties.agda b/FinMerge/Properties.agda
index 5f92905..6e9d53a 100644
--- a/FinMerge/Properties.agda
+++ b/FinMerge/Properties.agda
@@ -13,10 +13,11 @@ open import Data.Maybe.Base using (Maybe; map; nothing; just; fromMaybe)
 open import Function using (id;  _∘_)
 open import Relation.Binary.Definitions using (tri<; tri≈; tri>)
 
-open import Util using (_<_<_; _<_≤_; toℕ<; Ordering; less; equal; greater; compare)
+open import FinMerge.Util using (_<_≤_; Ordering; compare)
 
 open import FinMerge using (merge; unmerge; pluck; glue-once; glue-unglue-once; glue-iter; unpluck)
 
+open Ordering
 
 private
   variable
diff --git a/FinMerge/Util.agda b/FinMerge/Util.agda
new file mode 100644
index 0000000..6a7f7b4
--- /dev/null
+++ b/FinMerge/Util.agda
@@ -0,0 +1,32 @@
+{-# OPTIONS --without-K --safe #-}
+module FinMerge.Util where
+
+open import Data.Fin using (Fin; toℕ)
+open import Data.Nat using (ℕ; _≤_; _<_ ; z<s; s≤s)
+open import Data.Product using (_×_; _,_)
+open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
+
+
+_<_≤_ : ℕ → ℕ → ℕ → Set
+_<_≤_ i j k = (i < j) × (j ≤ k)
+
+_<_<_ : ℕ → ℕ → ℕ → Set
+_<_<_ i j k = (i < j) × (j < k)
+
+toℕ< : {n : ℕ} → (i : Fin n) → toℕ i < n
+toℕ< Fin.zero = z<s
+toℕ< (Fin.suc i) = s≤s (toℕ< i)
+
+data Ordering {n : ℕ} : Fin n → Fin n → Set where
+  less : ∀ {i j} → toℕ i < toℕ j < n → Ordering i j
+  equal : ∀ {i j} → i ≡ j → Ordering i j
+  greater : ∀ {i j} → toℕ j < toℕ i < n → Ordering i j
+
+compare : ∀ {n : ℕ} (i j : Fin n) → Ordering i j
+compare Fin.zero Fin.zero = equal refl
+compare Fin.zero j@(Fin.suc _) = less (z<s , toℕ< j)
+compare i@(Fin.suc _) Fin.zero = greater (z<s , toℕ< i)
+compare (Fin.suc i) (Fin.suc j) with compare i j
+... | less (i<j , j<n) = less (s≤s i<j , s≤s j<n)
+... | equal i≡j = equal (cong Fin.suc i≡j)
+... | greater (j<i , i<n) = greater (s≤s j<i , s≤s i<n)
diff --git a/Util.agda b/Util.agda
deleted file mode 100644
index d7053c5..0000000
--- a/Util.agda
+++ /dev/null
@@ -1,32 +0,0 @@
-{-# OPTIONS --without-K --safe #-}
-module Util where
-
-open import Data.Fin using (Fin; toℕ)
-open import Data.Nat using (ℕ; _≤_; _<_ ; z<s; s≤s)
-open import Data.Product using (_×_; _,_)
-open import Relation.Binary.PropositionalEquality using (_≡_; refl; cong)
-
-
-_<_≤_ : ℕ → ℕ → ℕ → Set
-_<_≤_ i j k = (i < j) × (j ≤ k)
-
-_<_<_ : ℕ → ℕ → ℕ → Set
-_<_<_ i j k = (i < j) × (j < k)
-
-toℕ< : {n : ℕ} → (i : Fin n) → toℕ i < n
-toℕ< Fin.zero = z<s
-toℕ< (Fin.suc i) = s≤s (toℕ< i)
-
-data Ordering {n : ℕ} : Fin n → Fin n → Set where
-  less : ∀ {i j} → toℕ i < toℕ j < n → Ordering i j
-  equal : ∀ {i j} → i ≡ j → Ordering i j
-  greater : ∀ {i j} → toℕ j < toℕ i < n → Ordering i j
-
-compare : ∀ {n : ℕ} (i j : Fin n) → Ordering i j
-compare Fin.zero Fin.zero = equal refl
-compare Fin.zero j@(Fin.suc _) = less (z<s , toℕ< j)
-compare i@(Fin.suc _) Fin.zero = greater (z<s , toℕ< i)
-compare (Fin.suc i) (Fin.suc j) with compare i j
-... | less (i<j , j<n) = less (s≤s i<j , s≤s j<n)
-... | equal i≡j = equal (cong Fin.suc i≡j)
-... | greater (j<i , i<n) = greater (s≤s j<i , s≤s i<n)
-- 
cgit v1.2.3