From e8bba1ebf3b73828b61d638e0cc796da98be4ace Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 25 Jan 2014 20:34:18 -0800
Subject: [PATCH] fix(frontends/lean/frontend): the definition of the explicit
 version @f must be definitionally equal to f

Before this commit, the explicit version @f of a constant f with implicit arguments as not definitionally equal to f.

For example, if we had

variable f {A : Type} : A -> Bool

Then, the definition of @f was

definition @f (A : Type) (a : A) : Bool := f A a

This definition is equivalent to
     fun A a, f A a
which is not definitionally equal to
     f
since definitionally equality in Lean ignores Eta conversion.

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/frontend.cpp        | 15 +--------------
 tests/lean/explicit2.lean              |  3 +++
 tests/lean/explicit2.lean.expected.out |  5 +++++
 3 files changed, 9 insertions(+), 14 deletions(-)
 create mode 100644 tests/lean/explicit2.lean
 create mode 100644 tests/lean/explicit2.lean.expected.out

diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index a04dab28e..0f405df64 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -318,19 +318,6 @@ struct lean_extension : public environment_extension {
         env->add_neutral_object(new notation_declaration(new_op, d));
     }
 
-    expr mk_explicit_definition_body(expr type, name const & n, unsigned i, unsigned sz) {
-        if (i == sz) {
-            buffer<expr> args;
-            args.push_back(mk_constant(n));
-            unsigned j = sz;
-            while (j > 0) { --j; args.push_back(mk_var(j)); }
-            return mk_app(args);
-        } else {
-            lean_assert(is_pi(type));
-            return mk_lambda(abst_name(type), abst_domain(type), mk_explicit_definition_body(abst_body(type), n, i+1, sz));
-        }
-    }
-
     static name mk_explicit_name(name const & n) {
         if (n.is_anonymous()) {
             throw exception("anonymous names cannot be used in definitions");
@@ -369,7 +356,7 @@ struct lean_extension : public environment_extension {
             throw exception(sstream() << "failed to mark implicit arguments for '" << n << "', all arguments are explicit");
         std::vector<bool> v(implicit, implicit+sz);
         m_implicit_table[n] = mk_pair(v, explicit_version);
-        expr body = mk_explicit_definition_body(type, n, 0, num_args);
+        expr body = mk_constant(n);
         m_explicit_names.insert(explicit_version);
         env->add_neutral_object(new mark_implicit_command(n, sz, implicit));
         env->auxiliary_section([&]() {
diff --git a/tests/lean/explicit2.lean b/tests/lean/explicit2.lean
new file mode 100644
index 000000000..35b10020d
--- /dev/null
+++ b/tests/lean/explicit2.lean
@@ -0,0 +1,3 @@
+variable f {A : Type} : A → A
+eval (@f Bool)
+eval @f
\ No newline at end of file
diff --git a/tests/lean/explicit2.lean.expected.out b/tests/lean/explicit2.lean.expected.out
new file mode 100644
index 000000000..b6d3e3f24
--- /dev/null
+++ b/tests/lean/explicit2.lean.expected.out
@@ -0,0 +1,5 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: f
+f
+@f