diff options
| author | Son Ho | 2023-09-07 16:06:14 +0200 |
|---|---|---|
| committer | Son Ho | 2023-09-07 16:06:14 +0200 |
| commit | ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 (patch) | |
| tree | 933d2bd806026930d216e4f16f113ea2749ca250 /tests/lean/BetreeMain | |
| parent | 1181aecddbcb3232c21b191fbde59c2e9596846a (diff) | |
Regenerate the test files and fix a proof
Diffstat (limited to 'tests/lean/BetreeMain')
| -rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean index 07ef08dc..6681731f 100644 --- a/tests/lean/BetreeMain/Funs.lean +++ b/tests/lean/BetreeMain/Funs.lean @@ -64,11 +64,6 @@ def betree.NodeIdCounter.fresh_id_back let i ← self.next_node_id + (U64.ofInt 1) Result.ret { next_node_id := i } -/- [core::num::u64::{9}::MAX] -/ -def core_num_u64_max_body : Result U64 := - Result.ret (U64.ofInt 18446744073709551615) -def core_num_u64_max_c : U64 := eval_global core_num_u64_max_body (by simp) - /- [betree_main::betree::upsert_update]: forward function -/ def betree.upsert_update (prev : Option U64) (st : betree.UpsertFunState) : Result U64 := @@ -81,10 +76,10 @@ def betree.upsert_update match st with | betree.UpsertFunState.Add v => do - let margin ← core_num_u64_max_c - prev0 + let margin ← core_u64_max - prev0 if margin >= v then prev0 + v - else Result.ret core_num_u64_max_c + else Result.ret core_u64_max | betree.UpsertFunState.Sub v => if prev0 >= v then prev0 - v |