summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon Ho2023-08-03 00:28:10 +0200
committerSon Ho2023-08-03 00:28:10 +0200
commitfa682c18c8ffc5fa7224d9e9d0e0dd94250ada57 (patch)
tree3edb80e8394601a5edc0efa604dd8f3a9d35fdd9 /tests/lean
parentfcbb06f1b32c42b42d6bde501a4bc29a661ec23b (diff)
Make a minor formatting modification for Lean
Diffstat (limited to '')
-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
14 files changed, 14 insertions, 0 deletions
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] -/