From c4367035ec0638d5639157e98e6756d3779aeee5 Mon Sep 17 00:00:00 2001 From: Jacques Comeaux Date: Sat, 6 Dec 2025 16:40:13 -0600 Subject: Move FinMerge utilites --- FinMerge/Properties.agda | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'FinMerge/Properties.agda') 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 -- cgit v1.2.3