fix: allow generalization in let (#3060)

As suggested by @kmill, removing an unnecessary `let` (possibly only
there in the first place for copy/paste reasons) seems to fix the
included test.

This makes `~q()` matching in quote4 noticeably more useful in things
like `norm_num` (as it fixes
leanprover-community/quote4#29)

It also makes a quote4 bug slightly more visible
(leanprover-community/quote4#30), but the bug
there already existed anyway, and isn't caused by this patch.

Fixes #3065

src/Lean/Elab/Do.lean

@@ -1368,7 +1368,7 @@ mutual
     else
       pure doElems.toArray
     let contSeq := mkDoSeq contSeq
-    let auxDo ← `(do let __discr := $val; match __discr with | $pattern:term => $contSeq | _ => $elseSeq)
+    let auxDo ← `(do match $val:term with | $pattern:term => $contSeq | _ => $elseSeq)
     doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
 
   /-- Generate `CodeBlock` for `doReassignArrow; doElems`

tests/lean/run/doLetElse.lean

@@ -3,10 +3,22 @@ def foo (x? : Option Nat) : IO Nat := do
   IO.println s!"x: {x}"
   return x
 
-def test (input : Option Nat) (expected : Nat) : IO Unit := do
+def testFoo (input : Option Nat) (expected : Nat) : IO Unit := do
   assert! (← foo input) == expected
 
+#eval testFoo (some 10) 10
+#eval testFoo none 0
+#eval testFoo (some 1) 1
 
-#eval test (some 10) 10
-#eval test none 0
-#eval test (some 1) 1
+def bar (x : Nat) : IO (Fin (x + 1)) := do
+  let 2 := x | return 0
+  -- the pattern match performed a substitution
+  let y : Fin 3 := ⟨1, by decide⟩
+  return y
+
+def testBar (x : Nat) (expected : Fin (x + 1)) : IO Unit := do
+  assert! (← bar x) == expected
+
+#eval testBar 1 0
+#eval testBar 2 1
+#eval testBar 3 0