feat: expand let-decls at decide!

src/Lean/Elab/BuiltinNotation.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 import Init.Data.ToString
 import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
+import Lean.Meta.Transform
 import Lean.Elab.Term
 import Lean.Elab.SyntheticMVars
 
@@ -135,7 +136,9 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
   | none => throwError "invalid macro, expected type is not available"
   | some expectedType =>
     synthesizeSyntheticMVars
-    let expectedType ← instantiateMVars expectedType
+    let mut expectedType ← instantiateMVars expectedType
+    if expectedType.hasFVar then
+      expectedType ← zetaReduce expectedType
     if expectedType.hasFVar || expectedType.hasMVar then
       throwError! "expected type must not contain free or meta variables{indentExpr expectedType}"
     pure expectedType
@@ -150,6 +153,7 @@ private def getPropToDecide (expectedType? : Option Expr) : TermElabM Expr := do
 
 @[builtinTermElab Lean.Parser.Term.decide] def elabDecide : TermElab := fun stx expectedType? => do
   let p ← getPropToDecide expectedType?
+  trace[Meta.debug]! "elabDecide: {p}"
   let d ← mkDecide p
   let d ← instantiateMVars d
   let s := d.appArg! -- get instance from `d`

src/Lean/Meta/Transform.lean

@@ -107,5 +107,20 @@ partial def transform {m} [Monad m] [MonadLiftT MetaM m] [MonadControlT MetaM m]
         | _                  => visitPost e
   visit input |>.run
 
+def zetaReduce (e : Expr) : MetaM Expr := do
+  let lctx ← getLCtx
+  let pre (e : Expr) : CoreM TransformStep := do
+    match e with
+    | Expr.fvar fvarId _ =>
+      match lctx.find? fvarId with
+      | none => return TransformStep.done e
+      | some localDecl =>
+        if let some value := localDecl.value? then
+          return TransformStep.visit value
+        else
+          return TransformStep.done e
+    | e => if e.hasFVar then return TransformStep.visit e else return TransformStep.done e
+  liftM (m := CoreM) <| Core.transform e (pre := pre)
+
 end Meta
 end Lean

tests/lean/run/decidelet.lean

@@ -0,0 +1,3 @@
+theorem ex : let x := 1; x < 2 := by
+  intro x
+  decide!