From a4decc7654bc6f3301c0174124d21fdbc2dbc708 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Sat, 23 Dec 2023 00:59:55 +0100
Subject: Regenerate the files

---
 tests/lean/External/Funs.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'tests/lean/External')

diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 88ced82d..db15aacc 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -25,8 +25,7 @@ def test_new_non_zero_u32
    Source: 'src/external.rs', lines 17:0-17:17 -/
 def test_vec : Result Unit :=
   do
-  let v := alloc.vec.Vec.new U32
-  let _ ← alloc.vec.Vec.push U32 v 0#u32
+  let _ ← alloc.vec.Vec.push U32 (alloc.vec.Vec.new U32) 0#u32
   Result.ret ()
 
 /- Unit test for [external::test_vec] -/
-- 
cgit v1.2.3