Mercurial > hg > Gears > GearsAgda

changeset 905:acee838690c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
caae2 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 31 May 2024 14:41:59 +0900
parents e86f6b9545fc
children a1b7703f8551
files hoareBinaryTree1.agda
diffstat 1 files changed, 0 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/hoareBinaryTree1.agda	Fri May 31 14:15:44 2024 +0900
+++ b/hoareBinaryTree1.agda	Fri May 31 14:41:59 2024 +0900
@@ -1976,10 +1976,6 @@
           length (RBI.tree r ∷ PG.parent pg ∷ PG.grand pg ∷ PG.rest pg) ≡⟨ cong length (sym (PG.stack=gp pg)) ⟩
           length stack ∎
              where open ≤-Reasoning
-
-
-          
-
 ... | s2-1sp2 {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-s12p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}
 ... | s2-1s2p {kp} {kg} {vp} {vg} {n1} {n2} x x₁ = {!!}