Mercurial > hg > Gears > GearsAgda
changeset 558:8595a7ffba8b
fix
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Mar 2018 18:38:40 +0900 |
| parents | 90999865d7f3 |
| children | cca54e32d7ac |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 16 insertions(+), 17 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Thu Mar 29 10:58:41 2018 +0900 +++ b/redBlackTreeTest.agda Thu Mar 29 18:38:40 2018 +0900 @@ -141,26 +141,25 @@ compareTri3 (suc m) eq = compareTri3 m (cong pred eq) compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m -compareTri4 zero {zero} eq _ = eq refl -compareTri4 zero {suc n} _ () -compareTri4 (suc m) {zero} _ () -compareTri4 (suc m) {suc n} neq with n ≟ m -... | yes p = λ q → neq ( cong suc p ) -... | no p = {!!} +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' zero () -compareTri4' (suc n) ≤′-refl () -compareTri4' (suc n) ( ≤′-step p ) = {!!} +<′dec : Set +<′dec = ∀ m n → Dec ( m ≤′ n ) + +is≤′ : <′dec +is≤′ zero zero = yes ≤′-refl +is≤′ zero (suc n) = yes {!!} +is≤′ (suc m) (zero) = no ( \ () ) +is≤′ (suc m) (suc n) with is≤′ m n +... | yes p = yes {!!} +... | no p = no {!!} compareTri5 : ∀ m {n} → ¬ m <′ n → ¬ suc m <′ suc n -compareTri5 zero neq = {!!} -compareTri5 (suc m) neq = {!!} - -compareTri5' : ∀ m {n} → m ≡ n → ¬ suc m <′ suc n -compareTri5' zero refl ( ≤′-step p ) = {!!} -compareTri5' (suc m) refl = {!!} - +compareTri5 m {n} with (is≤′ m n) +... | yes p = {!!} +... | no p = {!!} compareTri : Trichotomous _≡_ _<′_ compareTri zero zero = tri≈ ( λ ()) refl ( λ ())