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

feat: display mono phase code

Browse source
This commit is contained in:
Leonardo de Moura 2022-10-06 07:48:59 -07:00
parent 150022fe13
commit 9996686690
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -77,7 +77,7 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
if (← Lean.isTracingEnabledFor `Compiler.result) then
for decl in decls do
-- We display the declaration saved in the environment because the names have been normalized
let some decl' ← getDeclAt? decl.name .base | unreachable!
let some decl' ← getDeclAt? decl.name .mono | unreachable!
Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl'}"
return decls