feat(frontends/lean/definition_cmds): elaborate a def's type separately when explicit return type is given

library/init/core.lean

@@ -142,7 +142,7 @@ inductive false : Prop
 
 inductive empty : Type
 
-def not (a : Prop) := a → false
+def not (a : Prop) : Prop := a → false
 prefix `¬` := not
 
 inductive eq {α : Sort u} (a : α) : α → Prop

library/init/logic.lean

@@ -615,11 +615,11 @@ namespace decidable
   variables {p q : Prop}
 
   def rec_on_true [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : p) (h₄ : h₁ h₃)
-      : decidable.rec_on h h₂ h₁ :=
+      : (decidable.rec_on h h₂ h₁ : Sort u) :=
   decidable.rec_on h (λ h, false.rec _ (h h₃)) (λ h, h₄)
 
   def rec_on_false [h : decidable p] {h₁ : p → Sort u} {h₂ : ¬p → Sort u} (h₃ : ¬p) (h₄ : h₂ h₃)
-      : decidable.rec_on h h₂ h₁ :=
+      : (decidable.rec_on h h₂ h₁ : Sort u) :=
   decidable.rec_on h (λ h, h₄) (λ h, false.rec _ (h₃ h))
 
   def by_cases {q : Sort u} [φ : decidable p] : (p → q) → (¬p → q) → q := dite _

library/init/wf.lean

@@ -67,7 +67,7 @@ end well_founded
 open well_founded
 
 -- Empty relation is well-founded
-def empty_wf {α : Sort u} : well_founded empty_relation :=
+def empty_wf {α : Sort u} : well_founded (@empty_relation α) :=
 well_founded.intro (λ (a : α),
   acc.intro a (λ (b : α) (lt : false), false.rec _ lt))
 

old_tests/tests/lean/584a.lean

@@ -13,7 +13,7 @@ open nat
 
 #check foo nat 10
 
-definition test : foo' = (10:nat) := rfl
+definition test : @foo' ℕ _ 10 = (10:nat) := rfl
 
 set_option pp.implicit true
 #print test

src/frontends/lean/definition_cmds.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <vector>
+#include "library/placeholder.h"
 #include "library/time_task.h"
 #include "library/profiling.h"
 #include "library/library_task_builder.h"
@@ -586,7 +587,9 @@ static expr_pair elaborate_theorem(elaborator & elab, expr const & fn, expr val)
 }
 
 static expr_pair elaborate_definition_core(elaborator & elab, decl_cmd_kind kind, expr const & fn, expr const & val) {
-    if (kind == decl_cmd_kind::Theorem) {
+    // We elaborate `fn` and `val` separately if `fn` is a theorem or its return type
+    // was specified explicitly
+    if (kind == decl_cmd_kind::Theorem || !is_placeholder(mlocal_type(fn))) {
         return elaborate_theorem(elab, fn, val);
     } else {
         return elab.elaborate_with_type(val, mlocal_type(fn));