summaryrefslogtreecommitdiff
path: root/tests/lean/NoNestedBorrows.lean
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--tests/lean/NoNestedBorrows.lean1
1 files changed, 1 insertions, 0 deletions
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] -/