Mercurial > hg > Gears > GearsAgda
changeset 563:8634f448e699
minor fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 30 Mar 2018 11:09:06 +0900 |
| parents | 9df8103bc493 |
| children | 40ab3d39e49d |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 5 insertions(+), 2 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Fri Mar 30 10:52:51 2018 +0900 +++ b/redBlackTreeTest.agda Fri Mar 30 11:09:06 2018 +0900 @@ -176,11 +176,14 @@ compareTri3 zero () compareTri3 (suc m) eq = compareTri3 m (cong pred eq) -compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m -compareTri4 m {n} with n ≟ m +compareTri4' : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m +compareTri4' m {n} with n ≟ m ... | yes refl = λ x y → x refl ... | no p = λ x y → p ( cong pred y ) +compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m +compareTri4 m = contraposition ( λ x → cong pred x ) + -- compareTri6 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n compareTri6 m {n} = λ x y → x (compareTri21 _ _ y)