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 /FinMerge/Properties.agda | |
| parent | a643b7e119c5f086c67205072afaed3a1da2252e (diff) | |
Move FinMerge utilites
Diffstat (limited to 'FinMerge/Properties.agda')
| -rw-r--r-- | FinMerge/Properties.agda | 3 |
1 files changed, 2 insertions, 1 deletions
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 |