summaryrefslogtreecommitdiff
path: root/tests/lean/hashmap_on_disk
diff options
context:
space:
mode:
Diffstat (limited to 'tests/lean/hashmap_on_disk')
-rw-r--r--tests/lean/hashmap_on_disk/Base/Primitives.lean6
1 files changed, 2 insertions, 4 deletions
diff --git a/tests/lean/hashmap_on_disk/Base/Primitives.lean b/tests/lean/hashmap_on_disk/Base/Primitives.lean
index 71ce7153..3f1d13f1 100644
--- a/tests/lean/hashmap_on_disk/Base/Primitives.lean
+++ b/tests/lean/hashmap_on_disk/Base/Primitives.lean
@@ -1,6 +1,5 @@
import Lean
import Init.Data.List.Basic
-import Mathlib
-------------
-- PRELUDE --
@@ -155,12 +154,11 @@ def USize.checked_mul (n: USize) (m: USize): result USize :=
.fail integerOverflow
def USize.checked_div (n: USize) (m: USize): result USize :=
- if h: m > 0 then
+ if m > 0 then
.ret ⟨ n.val / m.val, by
- simp_arith
have h1: n.val < USize.size := n.val.isLt
have h2: n.val.val / m.val.val <= n.val.val := @Nat.div_le_self n.val m.val
- sorry
+ apply Nat.lt_of_le_of_lt h2 h1
else
.fail integerOverflow