diff options
Diffstat (limited to 'tests/lean')
-rw-r--r-- | tests/lean/BetreeMain/Funs.lean | 1 | ||||
-rw-r--r-- | tests/lean/BetreeMain/Types.lean | 1 | ||||
-rw-r--r-- | tests/lean/Constants.lean | 1 | ||||
-rw-r--r-- | tests/lean/External/Funs.lean | 1 | ||||
-rw-r--r-- | tests/lean/External/Types.lean | 1 | ||||
-rw-r--r-- | tests/lean/Hashmap/Funs.lean | 1 | ||||
-rw-r--r-- | tests/lean/Hashmap/Types.lean | 1 | ||||
-rw-r--r-- | tests/lean/HashmapMain/Funs.lean | 1 | ||||
-rw-r--r-- | tests/lean/HashmapMain/Types.lean | 1 | ||||
-rw-r--r-- | tests/lean/Loops/Funs.lean | 1 | ||||
-rw-r--r-- | tests/lean/Loops/Types.lean | 1 | ||||
-rw-r--r-- | tests/lean/NoNestedBorrows.lean | 1 | ||||
-rw-r--r-- | tests/lean/Paper.lean | 1 | ||||
-rw-r--r-- | tests/lean/PoloniusList.lean | 1 |
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] -/ |