fix(frontends/lean): bug in scope construct

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/environment_scope.cpp

@@ -59,7 +59,10 @@ static expr mk_ref(object const & obj, dependencies const & deps) {
         buffer<expr> args;
         args.push_back(mk_constant(obj.get_name()));
         for (auto d : deps) args.push_back(mk_constant(d));
-        return mk_app(args);
+        if (args.size() == 1)
+            return args[0];
+        else
+            return mk_app(args);
     }
 }
 

tests/lean/scope_bug1.lean

@@ -0,0 +1,18 @@
+variables a b c d : Nat
+axiom H : a + (b + c) = a + (b + d)
+
+set_option pp::implicit true
+
+using Nat
+check add_succr a
+
+scope
+
+theorem mul_zerol2 (a : Nat) : 0 * a = 0
+:= induction_on a
+    (have 0 * 0 = 0 : trivial)
+    (λ (n : Nat) (iH : 0 * n = 0),
+        calc  0 * (n + 1)  =  (0 * n) + 0 : mul_succr 0 n
+                      ...  =  0 + 0       : { iH }
+                      ...  =  0           : trivial)
+end

tests/lean/scope_bug1.lean.expected.out

@@ -0,0 +1,11 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: d
+  Assumed: H
+  Set: lean::pp::implicit
+  Using: Nat
+Nat::add_succr a : ∀ b : ℕ, @eq ℕ (a + (b + 1)) (a + b + 1)
+  Proved: mul_zerol2