From fd46ef01e8d8b4745369151a80e9bc3d959afdba Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 16 Oct 2022 08:51:13 -0700 Subject: [PATCH] chore: add another `floatLetIn` pass See `elabAppFn` for a function that benefits from this extra pass. --- src/Lean/Compiler/LCNF/Passes.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/src/Lean/Compiler/LCNF/Passes.lean b/src/Lean/Compiler/LCNF/Passes.lean index 3b9dd01b36..3a52f0aad7 100644 --- 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