From 5ca36bfc50083a01af2b7ae5f75993a520757ef5 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 15:17:58 +0200
Subject: Simplify the names used in Primitives.lean

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

(limited to 'tests/lean/External')

diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 10efc3db..3fc21d91 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -36,8 +36,8 @@ def test_new_non_zero_u32_fwd
 /- [external::test_vec] -/
 def test_vec_fwd : Result Unit :=
   do
-    let v := vec_new U32
-    let _ ← vec_push_back U32 v (U32.ofInt 0 (by intlit))
+    let v := Vec.new U32
+    let _ ← Vec.push U32 v (U32.ofInt 0 (by intlit))
     Result.ret ()
 
 /- Unit test for [external::test_vec] -/
-- 
cgit v1.2.3