max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: activate toMono compiler pass

Browse source 
It increases the .olean sizes.
This commit is contained in:
Leonardo de Moura 2022-10-06 05:44:59 -07:00
parent 80bf4f3334
commit faa30bccb2
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Compiler/LCNF/Passes.lean
View file

@ -12,6 +12,7 @@ import Lean.Compiler.LCNF.ReduceJpArity
import Lean.Compiler.LCNF.JoinPoints
import Lean.Compiler.LCNF.Specialize
import Lean.Compiler.LCNF.PhaseExt
import Lean.Compiler.LCNF.ToMono
namespace Lean.Compiler.LCNF
@ -49,7 +50,8 @@ def builtinPassManager : PassManager := {
specialize,
simp (occurrence := 2),
cse,
saveBase -- End of base phase
saveBase, -- End of base phase
toMono
]
}