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

chore: proper trace message class

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-31 11:04:42 -07:00
parent 2bd04285f8
commit 23f3de5061
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/Elab/PreDefinition/Eqns.lean
View file

@ -207,7 +207,7 @@ partial def mkEqnTypes (declNames : Array Name) (mvarId : MVarId) : MetaM (Array
return eqnTypes
where
go (mvarId : MVarId) : ReaderT Context (StateRefT (Array Expr) MetaM) Unit := do
trace[Elab.definition.structural.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
trace[Elab.definition.eqns] "mkEqnTypes step\n{MessageData.ofGoal mvarId}"
if (← tryURefl mvarId) then
saveEqn mvarId
return ()
@ -370,5 +370,6 @@ def getUnfoldFor? (declName : Name) (getInfo? : Unit → Option EqnInfoCore) : M
builtin_initialize
registerTraceClass `Elab.definition.unfoldEqn
registerTraceClass `Elab.definition.eqns
end Lean.Elab.Eqns