Reorganize the Lean tests

4 files changed, 10 insertions, 4 deletions

diff --git a/tests/lean/misc-external/External.lean b/tests/lean/External.lean
index b95db309..b95db309 100644
--- a/tests/lean/misc-external/External.lean
+++ b/tests/lean/External.lean
diff --git a/tests/lean/misc-external/External/Funs.lean b/tests/lean/External/Funs.lean
index eeb83989..73e45938 100644
--- a/tests/lean/misc-external/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -1,8 +1,9 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [external]: function definitions
-import Base.Primitives
+import Base
 import External.Types
 import External.ExternalFuns
+open Primitives
 
 /- [external::swap] -/
 def swap_fwd
@@ -39,6 +40,9 @@ def test_vec_fwd : Result Unit :=
     let _ ← vec_push_back U32 v (U32.ofInt 0 (by intlit))
     Result.ret ()
 
+/- Unit test for [external::test_vec] -/
+#assert (test_vec_fwd == .ret ())
+
 /- [external::custom_swap] -/
 def custom_swap_fwd
   (T : Type) (x : T) (y : T) (st : State) : Result (State × T) :=
@@ -78,7 +82,7 @@ def test_swap_non_zero_fwd (x : U32) (st : State) : Result (State × U32) :=
   do
     let (st0, _) ← swap_fwd U32 x (U32.ofInt 0 (by intlit)) st
     let (st1, (x0, _)) ← swap_back U32 x (U32.ofInt 0 (by intlit)) st st0
-    if h: x0 = (U32.ofInt 0 (by intlit))
+    if x0 = (U32.ofInt 0 (by intlit))
     then Result.fail Error.panic
     else Result.ret (st1, x0)
 
diff --git a/tests/lean/misc-external/External/Opaque.lean b/tests/lean/External/Opaque.lean
index d641912b..5483c3a9 100644
--- a/tests/lean/misc-external/External/Opaque.lean
+++ b/tests/lean/External/Opaque.lean
@@ -1,7 +1,8 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [external]: opaque function definitions
-import Base.Primitives
+import Base
 import External.Types
+open Primitives
 
 structure OpaqueDefs where
   
diff --git a/tests/lean/misc-external/External/Types.lean b/tests/lean/External/Types.lean
index ed1842be..25907da2 100644
--- a/tests/lean/misc-external/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -1,6 +1,7 @@
 -- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS
 -- [external]: type definitions
-import Base.Primitives
+import Base
+open Primitives
 
 /- [core::num::nonzero::NonZeroU32] -/
 axiom core_num_nonzero_non_zero_u32_t : Type