Make a minor formatting modification for Lean

1 files changed, 1 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";