chore: add another floatLetIn pass

See `elabAppFn` for a function that benefits from this extra pass.
2022-10-16 08:51:13 -07:00 · 2022-10-16 08:51:13 -07:00 · fd46ef01e8
commit fd46ef01e8
parent ae627e9a58
1 changed files with 1 additions and 0 deletions
--- a/src/Lean/Compiler/LCNF/Passes.lean
+++ b/src/Lean/Compiler/LCNF/Passes.lean
@ -61,6 +61,7 @@ def builtinPassManager : PassManager := {
    extendJoinPointContext,
    floatLetIn (phase := .mono) (occurrence := 1),
    simp (occurrence := 4) (phase := .mono),
+    floatLetIn (phase := .mono) (occurrence := 2),
    lambdaLifting,
    simp (occurrence := 5) (phase := .mono),
    -- TODO: reduce function arity