Mercurial > hg > Gears > GearsAgda
changeset 557:90999865d7f3
some try ..
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 29 Mar 2018 10:58:41 +0900 |
| parents | 69fc15bb4e82 |
| children | 8595a7ffba8b |
| files | redBlackTreeTest.agda |
| diffstat | 1 files changed, 16 insertions(+), 3 deletions(-) [+] |
line wrap: on
line diff
--- a/redBlackTreeTest.agda Tue Mar 27 09:30:49 2018 +0900 +++ b/redBlackTreeTest.agda Thu Mar 29 10:58:41 2018 +0900 @@ -141,13 +141,26 @@ compareTri3 (suc m) eq = compareTri3 m (cong pred eq) compareTri4 : ∀ m {n} → ¬ n ≡ m → ¬ suc n ≡ suc m -compareTri4 zero neq = {!!} -compareTri4 (suc m) neq = {!!} +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 = {!!} -compareTri5 : ∀ m {n} → ¬ m ≤′ n → ¬ suc m ≤′ suc n +compareTri4' : ∀ m {n} → n <′ m → ¬ suc n ≡ suc m +compareTri4' zero () +compareTri4' (suc n) ≤′-refl () +compareTri4' (suc n) ( ≤′-step p ) = {!!} + +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 = {!!} + compareTri : Trichotomous _≡_ _<′_ compareTri zero zero = tri≈ ( λ ()) refl ( λ ())