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

chore: add trace class `Elab.definition

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-15 12:01:18 -08:00
parent 41992c4bb2
commit f280ad401a
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Lean/Elab/Definition.lean
View file

@ -98,6 +98,7 @@ else withUsedWhen ref vars xs val type view.kind.isDefOrOpaque $ fun vars => do
val ← Term.levelMVarToParam val;
type ← Term.instantiateMVars ref type;
val ← Term.instantiateMVars view.val val;
Term.trace `Elab.definition.body ref $ fun _ => val;
let usedParams : CollectLevelParams.State := {};
let usedParams := collectLevelParams usedParams type;
let usedParams := collectLevelParams usedParams val;
@ -153,6 +154,10 @@ withDeclId view.declId $ fun name => do
compileDecl ref decl;
applyAttributes ref declName view.modifiers.attrs AttributeApplicationTime.afterCompilation
@[init] private def regTraceClasses : IO Unit := do
registerTraceClass `Elab.definition;
pure ()
end Command
end Elab
end Lean