From dee74ca1f90acb076289286f6f69df65e63604ce Mon Sep 17 00:00:00 2001
From: Jonathan Protzenko
Date: Mon, 23 Jan 2023 18:43:45 -0800
Subject: Write a tactic to discharge integer literal proof obligations

---
 tests/lean/hashmap_on_disk/Hashmap/Funs.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests/lean/hashmap_on_disk/Hashmap/Funs.lean')

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
-- 
cgit v1.2.3