15 files changed, 15 insertions, 1 deletions
diff --git a/compiler/Translate.ml b/compiler/Translate.ml
index c5f7df92..17355dfd 100644
--- a/compiler/Translate.ml
+++ b/compiler/Translate.ml
@@ -855,7 +855,7 @@ let extract_file (config : gen_config) (ctx : gen_ctx) (fi : extract_file_info)
       (* Always open the Primitives namespace *)
       Printf.fprintf out "open Primitives\n";
       (* If we are inside the namespace: declare it, otherwise: open it *)
-      if fi.in_namespace then Printf.fprintf out "namespace %s\n" fi.namespace
+      if fi.in_namespace then Printf.fprintf out "\nnamespace %s\n" fi.namespace
       else Printf.fprintf out "open %s\n" fi.namespace
   | HOL4 ->
       Printf.fprintf out "open primitivesLib divDefLib\n";
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 142adf08..a6c6f496 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -4,6 +4,7 @@ import Base
 import BetreeMain.Types
 import BetreeMain.FunsExternal
 open Primitives
+
 namespace betree_main
 
 /- [betree_main::betree::load_internal_node]: forward function -/
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index 783ade64..c02c148a 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -2,6 +2,7 @@
 -- [betree_main]: type definitions
 import Base
 open Primitives
+
 namespace betree_main
 
 /- [betree_main::betree::List] -/
diff --git a/tests/lean/Constants.lean b/tests/lean/Constants.lean
index 4a5a7b8f..ec07d0fe 100644
--- a/tests/lean/Constants.lean
+++ b/tests/lean/Constants.lean
@@ -2,6 +2,7 @@
 -- [constants]
 import Base
 open Primitives
+
 namespace constants
 
 /- [constants::X0] -/
diff --git a/tests/lean/External/Funs.lean b/tests/lean/External/Funs.lean
index 674aaebd..055d7860 100644
--- a/tests/lean/External/Funs.lean
+++ b/tests/lean/External/Funs.lean
@@ -4,6 +4,7 @@ import Base
 import External.Types
 import External.FunsExternal
 open Primitives
+
 namespace external
 
 /- [external::swap]: forward function -/
diff --git a/tests/lean/External/Types.lean b/tests/lean/External/Types.lean
index ba984e2a..71d70eed 100644
--- a/tests/lean/External/Types.lean
+++ b/tests/lean/External/Types.lean
@@ -2,6 +2,7 @@
 -- [external]: type definitions
 import Base
 open Primitives
+
 namespace external
 
 /- [core::num::nonzero::NonZeroU32] -/
diff --git a/tests/lean/Hashmap/Funs.lean b/tests/lean/Hashmap/Funs.lean
index 870693b5..2fa981ce 100644
--- a/tests/lean/Hashmap/Funs.lean
+++ b/tests/lean/Hashmap/Funs.lean
@@ -3,6 +3,7 @@
 import Base
 import Hashmap.Types
 open Primitives
+
 namespace hashmap
 
 /- [hashmap::hash_key]: forward function -/
diff --git a/tests/lean/Hashmap/Types.lean b/tests/lean/Hashmap/Types.lean
index 6606cf9e..6455798d 100644
--- a/tests/lean/Hashmap/Types.lean
+++ b/tests/lean/Hashmap/Types.lean
@@ -2,6 +2,7 @@
 -- [hashmap]: type definitions
 import Base
 open Primitives
+
 namespace hashmap
 
 /- [hashmap::List] -/
diff --git a/tests/lean/HashmapMain/Funs.lean b/tests/lean/HashmapMain/Funs.lean
index 610bae46..ea28b03f 100644
--- a/tests/lean/HashmapMain/Funs.lean
+++ b/tests/lean/HashmapMain/Funs.lean
@@ -4,6 +4,7 @@ import Base
 import HashmapMain.Types
 import HashmapMain.FunsExternal
 open Primitives
+
 namespace hashmap_main
 
 /- [hashmap_main::hashmap::hash_key]: forward function -/
diff --git a/tests/lean/HashmapMain/Types.lean b/tests/lean/HashmapMain/Types.lean
index 3b3d0d7c..2b5cbd6c 100644
--- a/tests/lean/HashmapMain/Types.lean
+++ b/tests/lean/HashmapMain/Types.lean
@@ -2,6 +2,7 @@
 -- [hashmap_main]: type definitions
 import Base
 open Primitives
+
 namespace hashmap_main
 
 /- [hashmap_main::hashmap::List] -/
diff --git a/tests/lean/Loops/Funs.lean b/tests/lean/Loops/Funs.lean
index f7e6603d..fac0c5a9 100644
--- a/tests/lean/Loops/Funs.lean
+++ b/tests/lean/Loops/Funs.lean
@@ -3,6 +3,7 @@
 import Base
 import Loops.Types
 open Primitives
+
 namespace loops
 
 /- [loops::sum]: loop 0: forward function -/
diff --git a/tests/lean/Loops/Types.lean b/tests/lean/Loops/Types.lean
index f8bc193b..018af901 100644
--- a/tests/lean/Loops/Types.lean
+++ b/tests/lean/Loops/Types.lean
@@ -2,6 +2,7 @@
 -- [loops]: type definitions
 import Base
 open Primitives
+
 namespace loops
 
 /- [loops::List] -/
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index bc707fd9..1a180c60 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -2,6 +2,7 @@
 -- [no_nested_borrows]
 import Base
 open Primitives
+
 namespace no_nested_borrows
 
 /- [no_nested_borrows::Pair] -/
diff --git a/tests/lean/Paper.lean b/tests/lean/Paper.lean
index cee7128a..c15c5e4b 100644
--- a/tests/lean/Paper.lean
+++ b/tests/lean/Paper.lean
@@ -2,6 +2,7 @@
 -- [paper]
 import Base
 open Primitives
+
 namespace paper
 
 /- [paper::ref_incr]: merged forward/backward function
diff --git a/tests/lean/PoloniusList.lean b/tests/lean/PoloniusList.lean
index 1453c275..07f206a8 100644
--- a/tests/lean/PoloniusList.lean
+++ b/tests/lean/PoloniusList.lean
@@ -2,6 +2,7 @@
 -- [polonius_list]
 import Base
 open Primitives
+
 namespace polonius_list
 
 /- [polonius_list::List] -/