summaryrefslogtreecommitdiff
path: root/tests/lean/BetreeMain/Funs.lean
diff options
context:
space:
mode:
authorSon Ho2024-04-04 11:58:44 +0200
committerSon Ho2024-04-04 11:58:44 +0200
commit975ddb208f18cb4ba46293dd788c46eb1ce43938 (patch)
treefe3c083f8c180f71bdc1ac8f22c1aaff51c30671 /tests/lean/BetreeMain/Funs.lean
parent795e2107e305d425efdf6071b29f186cae83656b (diff)
Regenerate the test files
Diffstat (limited to '')
-rw-r--r--tests/lean/BetreeMain/Funs.lean12
1 files changed, 6 insertions, 6 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index ca9b48da..2fbcd6a4 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -192,12 +192,12 @@ divergent def betree.Node.lookup_first_message_for_key
do
let (l, lookup_first_message_for_key_back) ←
betree.Node.lookup_first_message_for_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_for_key_back ret
Result.ret (betree.List.Cons (i, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
@@ -364,12 +364,12 @@ divergent def betree.Node.lookup_first_message_after_key
do
let (l, lookup_first_message_after_key_back) ←
betree.Node.lookup_first_message_after_key key next_msgs
- let back_'a :=
+ let back :=
fun ret =>
do
let next_msgs1 ← lookup_first_message_after_key_back ret
Result.ret (betree.List.Cons (k, m) next_msgs1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
@@ -468,12 +468,12 @@ divergent def betree.Node.lookup_mut_in_bindings
do
let (l, lookup_mut_in_bindings_back) ←
betree.Node.lookup_mut_in_bindings key tl
- let back_'a :=
+ let back :=
fun ret =>
do
let tl1 ← lookup_mut_in_bindings_back ret
Result.ret (betree.List.Cons (i, i1) tl1)
- Result.ret (l, back_'a)
+ Result.ret (l, back)
| betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: