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

fix: typo in trace class name

Browse source
This commit is contained in:
Gabriel Ebner 2023-02-10 12:27:23 -08:00
parent e6b3202df3
commit 1f61633da7
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/Meta/ExprDefEq.lean
View file

@ -1811,7 +1811,7 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
builtin_initialize
registerTraceClass `Meta.isDefEq
registerTraceClass `Meta.isDefEq.stuck
registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true)
registerTraceClass `Meta.isDefEq.stuckMVar (inherited := true)
registerTraceClass `Meta.isDefEq.cache
registerTraceClass `Meta.isDefEq.foApprox (inherited := true)
registerTraceClass `Meta.isDefEq.onFailure (inherited := true)