Mercurial > hg > Gears > GearsAgda
changeset 595:0927df986552
fix
| author | ryokka |
|---|---|
| date | Thu, 16 Jan 2020 16:04:59 +0900 |
| parents | 4bbeb8d9e250 |
| children | 4be84ddbf593 |
| files | hoareBinaryTree.agda |
| diffstat | 1 files changed, 7 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- a/hoareBinaryTree.agda Wed Jan 15 20:50:50 2020 +0900 +++ b/hoareBinaryTree.agda Thu Jan 16 16:04:59 2020 +0900 @@ -95,6 +95,13 @@ reverse した stack を使って find をチェックするかんじ? --} +tree+stack : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) + → (stack : List (bt'-path A )) → Set n +tree+stack tree mtree [] = tree ≡ mtree +tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-left key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack) +tree+stack {n} {m} {A} {t} {tn} tree mtree (bt'-right key x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack {n} {_} {_} {_} {tn} tree {!!} stack) +-- tree+stack tree mtree (bt'-right key {rkey} x x₁ ∷ stack) = (mtree ≡ {!!}) ∧ (tree+stack tree {!!} stack) -- tn ≡ rkey がひつよう + tree+stack≡tree : {n m : Level} {A : Set n} {t : Set m} {tn : ℕ} → (tree mtree : bt' A tn ) → (stack : List (bt'-path A )) → (reverse stack) ≡ {!!} tree+stack≡tree tree (bt'-leaf key) stack = {!!}