diff options
| author | Jonathan Protzenko | 2023-01-31 12:46:26 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | b30bac9e20735ab47327a2ac3122c2cfce162845 (patch) | |
| tree | 910a10ac4b18cf43b7b80fc5f84be709e3afca7f /tests/lean/hashmap_on_disk/Base | |
| parent | 3a67a4174e291c0b88537415c01fe2ada90e1ca0 (diff) | |
Remove last sorry in Primitives
Diffstat (limited to 'tests/lean/hashmap_on_disk/Base')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Base/Primitives.lean | 6 |
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 |