test(tests/lean): add new test for scoping rules

tests/lean/sec2.lean

@@ -0,0 +1,24 @@
+structure A : Type := mk
+structure B : Type := mk
+constant f : A → B
+constant g : B → B
+constant a : A
+
+namespace foo
+  coercion f
+  print coercions
+  check g a
+end foo
+
+check g a -- Error
+
+section boo
+  coercion f
+  print coercions
+  check g a
+end boo
+-- The metaobjects defined in the section persist to the outer level.
+-- This is not a bug. The idea is: we can use the scope to define
+-- auxiliary variables that are then used to define classes/instances/etc.
+-- That is, the whole point of the scope is to define these metaobjects.
+check g a -- Ok

tests/lean/sec2.lean.expected.out

@@ -0,0 +1,13 @@
+A ↣ B : f
+g a : B
+sec2.lean:13:6: error: type mismatch at application
+  g a
+term
+  a
+has type
+  A
+but is expected to have type
+  B
+A ↣ B : f
+g a : B
+g a : B