diff --git a/tests/lean/sec_notation2.lean b/tests/lean/sec_notation2.lean
new file mode 100644
index 000000000..8a3610a9b
--- /dev/null
+++ b/tests/lean/sec_notation2.lean
@@ -0,0 +1,36 @@
+open nat
+
+namespace foo
+
+section
+  section
+    parameter (A : Type)
+    definition f (a b : A) : A := a
+
+    definition add2 (a : nat) : nat := a + 2
+
+    postfix `+.2`:100 := add2
+
+    local postfix `++2`:100 := add2
+
+    eval 3 +.2
+
+    example : 3 +.2 = 3 ++2 := rfl
+ end
+
+ eval 3 +.2
+
+ example : 3 +.2 = 3 ++2 := rfl -- error
+
+end
+
+ eval 3 +.2
+end foo
+
+example : 3 +.2 = 5 := -- error
+rfl
+
+open foo
+
+example : 3 +.2 = 5 := -- error
+rfl
diff --git a/tests/lean/sec_notation2.lean.expected.out b/tests/lean/sec_notation2.lean.expected.out
new file mode 100644
index 000000000..4cf4a1a32
--- /dev/null
+++ b/tests/lean/sec_notation2.lean.expected.out
@@ -0,0 +1,5 @@
+5
+5
+sec_notation2.lean:23:21: error: invalid expression
+5
+sec_notation2.lean:30:13: error: invalid expression