Mercurial > hg > Gears > GearsAgda

diff 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
line wrap: on
line diff
--- a/hoareBinaryTree.agda	Tue Nov 09 09:44:23 2021 +0900
+++ b/hoareBinaryTree.agda	Wed Nov 10 10:18:34 2021 +0900
@@ -196,7 +196,7 @@
      tree0 : bt A
      ti : treeInvariant tree0
      si : stackInvariant key tree tree0 stack
-     ci : C tree stack
+     ci : C tree stack     -- data continuation
    
 findPP : {n m : Level} {A : Set n} {t : Set m}
            → (key : ℕ) → (tree : bt A ) → (stack : List (bt A))