feat: support let rec in #eval (#5663)

Makes `#eval` use the `elabMutualDef` machinery to process all the `let
rec`s that might appear in the expression. This now works:
```lean
#eval
  let rec fact (n : Nat) : Nat :=
    match n with
    | 0 => 1
    | n' + 1 => n * fact n'
  fact 5
```

Closes #2374

src/Lean/Elab/BuiltinEvalCommand.lean

@@ -4,11 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kyle Miller
 -/
 prelude
-import Lean.Util.CollectLevelParams
 import Lean.Util.CollectAxioms
-import Lean.Meta.Reduce
-import Lean.Elab.Eval
 import Lean.Elab.Deriving.Basic
+import Lean.Elab.MutualDef
 
 /-!
 # Implementation of `#eval` command
@@ -81,19 +79,15 @@ where
     return mkAppN m args
 
 private def addAndCompileExprForEval (declName : Name) (value : Expr) (allowSorry := false) : TermElabM Unit := do
-  let value ← Term.levelMVarToParam (← instantiateMVars value)
-  let type ← inferType value
-  let us := collectLevelParams {} value |>.params
-  let decl := Declaration.defnDecl {
-    name        := declName
-    levelParams := us.toList
-    type        := type
-    value       := value
-    hints       := ReducibilityHints.opaque
-    safety      := DefinitionSafety.unsafe
-  }
-  Term.ensureNoUnassignedMVars decl
-  addAndCompile decl
+  -- Use the `elabMutualDef` machinery to be able to support `let rec`.
+  -- Hack: since we are using the `TermElabM` version, we can insert the `value` as a metavariable via `exprToSyntax`.
+  -- An alternative design would be to make `elabTermForEval` into a term elaborator and elaborate the command all at once
+  -- with `unsafe def _eval := term_for_eval% $t`, which we did try, but unwanted error messages
+  -- such as "failed to infer definition type" can surface.
+  let defView := mkDefViewOfDef { isUnsafe := true }
+    (← `(Parser.Command.definition|
+          def $(mkIdent <| `_root_ ++ declName) := $(← Term.exprToSyntax value)))
+  Term.elabMutualDef #[] { header := "" } #[defView]
   unless allowSorry do
     let axioms ← collectAxioms declName
     if axioms.contains ``sorryAx then

tests/lean/run/eval.lean

@@ -177,3 +177,19 @@ info: hi
 error: ex
 -/
 #guard_msgs in #eval throwsEx
+
+/-!
+Let rec support (issue #2374)
+-/
+/-- info: 37 : Nat -/
+#guard_msgs in #eval
+  let rec bar : Nat := 1
+  37
+
+/-- info: 120 : Nat -/
+#guard_msgs in #eval
+  let rec fact (n : Nat) : Nat :=
+    match n with
+    | 0 => 1
+    | n' + 1 => n * fact n'
+  fact 5

tests/lean/run/meta5.lean

@@ -28,11 +28,11 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3014 : Nat
-[Meta.debug] ?_uniq.3015 : Nat →
+[Meta.debug] ?_uniq.3019 : Nat →
       Nat →
         let x := 0;
         Nat
+[Meta.debug] ?_uniq.3018 : Nat
 -/
 #guard_msgs in
 #eval tst1