diff options
| author | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-04-23 17:45:31 -0500 |
|---|---|---|
| committer | Jacques Comeaux <jacquesrcomeaux@protonmail.com> | 2024-04-23 17:45:31 -0500 |
| commit | ce4ea63db5e11b150058894f98b4a36a3003c95a (patch) | |
| tree | 600ef448bb7f5b541cb1f532f0ad272d7b05e9e4 /Util.agda | |
| parent | 37aef854206076a42c26cc021c97bb2c334b9424 (diff) | |
Add merge and unmerge properties
Diffstat (limited to 'Util.agda')
| -rw-r--r-- | Util.agda | 4 |
1 files changed, 2 insertions, 2 deletions
@@ -27,6 +27,6 @@ compare Fin.zero Fin.zero = equal refl compare Fin.zero j@(Fin.suc _) = less (z<s , toℕ< j) compare i@(Fin.suc _) Fin.zero = greater (z<s , toℕ< i) compare (Fin.suc i) (Fin.suc j) with compare i j -... | less (i<j , j<n) = less (_≤_.s≤s i<j , _≤_.s≤s j<n) +... | less (i<j , j<n) = less (s≤s i<j , s≤s j<n) ... | equal i≡j = equal (cong Fin.suc i≡j) -... | greater (j<i , i<n) = greater (_≤_.s≤s j<i , _≤_.s≤s i<n) +... | greater (j<i , i<n) = greater (s≤s j<i , s≤s i<n) |