summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--compiler/Translate.ml2
-rw-r--r--tests/lean/BetreeMain/Funs.lean1
-rw-r--r--tests/lean/BetreeMain/Types.lean1
-rw-r--r--tests/lean/Constants.lean1
-rw-r--r--tests/lean/External/Funs.lean1
-rw-r--r--tests/lean/External/Types.lean1
-rw-r--r--tests/lean/Hashmap/Funs.lean1
-rw-r--r--tests/lean/Hashmap/Types.lean1
-rw-r--r--tests/lean/HashmapMain/Funs.lean1
-rw-r--r--tests/lean/HashmapMain/Types.lean1
-rw-r--r--tests/lean/Loops/Funs.lean1
-rw-r--r--tests/lean/Loops/Types.lean1
-rw-r--r--tests/lean/NoNestedBorrows.lean1
-rw-r--r--tests/lean/Paper.lean1
-rw-r--r--tests/lean/PoloniusList.lean1
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] -/