diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-02-20 21:23:29 -0600 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-02-20 21:23:29 -0600 |
| commit | 5e30f210d4d510649ca87a02b7e9a409ee74d13a (patch) | |
| tree | b8e0b88f115888a0923a43f54dd5c2d4505cb3c0 /FinMerge.agda | |
| parent | e585420fc6eb90f0ecdce76e1f48085b2cfe0466 (diff) | |
Prove merge lemmas
Diffstat (limited to 'FinMerge.agda')
| -rw-r--r-- | FinMerge.agda | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/FinMerge.agda b/FinMerge.agda index b483fc8..f237a53 100644 --- a/FinMerge.agda +++ b/FinMerge.agda @@ -12,16 +12,8 @@ open import Relation.Binary.PropositionalEquality.Properties using (module ≡-R open import Function using (id ; _∘_ ; _$_) open import Data.Maybe.Base using (Maybe; just; nothing; fromMaybe) +open import Util using (_<_<_; _<_≤_; toℕ<) -_<_≤_ : ℕ → ℕ → ℕ → 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 |