From 468e6a68ea2b9084badaf689cc9d1c11726b538d Mon Sep 17 00:00:00 2001
From: Kyle Miller <kmill31415@gmail.com>
Date: Wed, 9 Oct 2024 13:38:30 -0700
Subject: [PATCH] feat: support `let rec` in `#eval`

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 | 23 +++++++----------------
 tests/lean/run/eval.lean              | 16 ++++++++++++++++
 2 files changed, 23 insertions(+), 16 deletions(-)

diff --git a/src/Lean/Elab/BuiltinEvalCommand.lean b/src/Lean/Elab/BuiltinEvalCommand.lean
index f5cb0179ba354..3e4620016b73b 100644
--- a/src/Lean/Elab/BuiltinEvalCommand.lean
+++ b/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,12 @@ 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`.
+  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
diff --git a/tests/lean/run/eval.lean b/tests/lean/run/eval.lean
index f098698cb6c50..3be84565e5eef 100644
--- a/tests/lean/run/eval.lean
+++ b/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