diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-06 16:40:13 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2025-12-06 16:40:13 -0600 |
| commit | c4367035ec0638d5639157e98e6756d3779aeee5 (patch) | |
| tree | 759df27c7cc7fac5a2e9a4324749d8d046841077 | |
| parent | a643b7e119c5f086c67205072afaed3a1da2252e (diff) | |
Move FinMerge utilites
| -rw-r--r-- | FinMerge.agda | 3 | ||||
| -rw-r--r-- | FinMerge/Properties.agda | 3 | ||||
| -rw-r--r-- | FinMerge/Util.agda (renamed from Util.agda) | 2 |
3 files changed, 5 insertions, 3 deletions
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/Util.agda b/FinMerge/Util.agda index d7053c5..6a7f7b4 100644 --- a/Util.agda +++ b/FinMerge/Util.agda @@ -1,5 +1,5 @@ {-# OPTIONS --without-K --safe #-} -module Util where +module FinMerge.Util where open import Data.Fin using (Fin; toℕ) open import Data.Nat using (ℕ; _≤_; _<_ ; z<s; s≤s) |