diff options
| -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) |