diff options
| author | Jonathan Protzenko | 2023-01-23 18:43:45 -0800 |
|---|---|---|
| committer | Son HO | 2023-06-04 21:44:33 +0200 |
| commit | dee74ca1f90acb076289286f6f69df65e63604ce (patch) | |
| tree | 50ddfb09bf11b20a688021c2413f45213c2c2450 /tests/lean/hashmap_on_disk/Hashmap/Funs.lean | |
| parent | 262cb9d72593b349af522596cbae29dff03525ea (diff) | |
Write a tactic to discharge integer literal proof obligations
Diffstat (limited to 'tests/lean/hashmap_on_disk/Hashmap/Funs.lean')
| -rw-r--r-- | tests/lean/hashmap_on_disk/Hashmap/Funs.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean index a4f2e3e0..c67a37ff 100644 --- a/tests/lean/hashmap_on_disk/Hashmap/Funs.lean +++ b/tests/lean/hashmap_on_disk/Hashmap/Funs.lean @@ -15,10 +15,10 @@ def hashmap_hash_map_allocate_slots_loop_fwd (T : Type) (slots : vec (hashmap_list_t T)) (n : USize) : result (vec (hashmap_list_t T)) := - if n > (USize.ofNatCore 0 (by simp)) + if n > (USize.ofNatCore 0 (by intlit)) then do let slots0: vec (hashmap_list_t T) <- @vec_push_back (hashmap_list_t T) slots HashmapListNil - let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by simp)) + let n0 <- USize.checked_sub n (USize.ofNatCore 1 (by intlit)) hashmap_hash_map_allocate_slots_loop_fwd T slots0 n0 else ret slots termination_by hashmap_hash_map_allocate_slots_loop_fwd _ _ n => n |