perf: always zeta reduce let expressions in cbv (#12397)

This PR adds zeta reduction simproc to the pre step of `cbv`.
2026-02-09 18:45:58 +00:00 · 2026-02-09 18:45:58 +00:00 · af2444a140
commit af2444a140
parent 57c5efe309
1 changed files with 1 additions and 1 deletions
--- a/src/Lean/Meta/Tactic/Cbv/Main.lean
+++ b/src/Lean/Meta/Tactic/Cbv/Main.lean
@ -145,7 +145,7 @@ def cbvPre : Simproc :=
      isBuiltinValue <|> isProofTerm <|> skipBinders
  >>  isOpaqueApp
  >>  simpControlCbv
-    <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj)
+    <|> ((isOpaqueConst >> handleConst) <|> simplifyAppFn <|> handleProj) <|> zetaReduce

 def cbvPost : Simproc :=
      evalGround