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

chore: only check if compiler.check is set to true

Browse source
This commit is contained in:
Leonardo de Moura 2022-09-01 07:18:47 -07:00
parent cedf9e980b
commit 29eddad325
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/Lean/Compiler/LCNF/Main.lean
View file

@ -49,7 +49,8 @@ def checkpoint (stepName : Name) (decls : Array Decl) : CompilerM Unit := do
Lean.addTrace clsName m!"size: {decl.size}\n{← ppDecl decl}"
if compiler.check.get (← getOptions) then
decl.check
checkDeadLocalDecls decls
if compiler.check.get (← getOptions) then
checkDeadLocalDecls decls
namespace PassManager