Mercurial > hg > Gears > GearsAgda

comparison hoareBinaryTree.agda @ 631:956ee8ae42b9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 10 Nov 2021 10:18:34 +0900
parents 24bec7639079
children b58991f8e2e4
comparison
equal deleted inserted replaced
630:24bec7639079 631:956ee8ae42b9
194 record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where 194 record findPR {n : Level} {A : Set n} (key : ℕ) (tree : bt A ) (stack : List (bt A)) (C : bt A → List (bt A) → Set n) : Set n where
195 field 195 field
196 tree0 : bt A 196 tree0 : bt A
197 ti : treeInvariant tree0 197 ti : treeInvariant tree0
198 si : stackInvariant key tree tree0 stack 198 si : stackInvariant key tree tree0 stack
199 ci : C tree stack 199 ci : C tree stack -- data continuation
200 200
201 findPP : {n m : Level} {A : Set n} {t : Set m} 201 findPP : {n m : Level} {A : Set n} {t : Set m}
202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A)) 202 → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))
203 → (Pre : findPR key tree stack (λ t s → Lift n ⊤)) 203 → (Pre : findPR key tree stack (λ t s → Lift n ⊤))
204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t ) 204 → (next : (tree1 : bt A) → (stack1 : List (bt A)) → findPR key tree1 stack1 (λ t s → Lift n ⊤) → bt-depth tree1 < bt-depth tree → t )