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

chore: register missing trace options, and fix inherited parameter

Browse source 
The current setting was bad for debugging `isDefEq` issues.
This commit is contained in:
Leonardo de Moura 2022-11-22 13:32:50 -08:00
parent cbf7da0f6e
commit dfaf9c6ebd
1 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Lean/Meta/ExprDefEq.lean
View file

@ -1756,11 +1756,23 @@ partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecD
builtin_initialize
registerTraceClass `Meta.isDefEq
registerTraceClass `Meta.isDefEq.foApprox
registerTraceClass `Meta.isDefEq.constApprox
registerTraceClass `Meta.isDefEq.delta (inherited := true)
registerTraceClass `Meta.isDefEq.stuck
registerTraceClass `Meta.isDefEq.stuck.mvar (inherited := true)
registerTraceClass `Meta.isDefEq.cache
registerTraceClass `Meta.isDefEq.foApprox (inherited := true)
registerTraceClass `Meta.isDefEq.onFailure (inherited := true)
registerTraceClass `Meta.isDefEq.constApprox (inherited := true)
registerTraceClass `Meta.isDefEq.delta
registerTraceClass `Meta.isDefEq.delta.unfoldLeft (inherited := true)
registerTraceClass `Meta.isDefEq.delta.unfoldRight (inherited := true)
registerTraceClass `Meta.isDefEq.delta.unfoldLeftRight (inherited := true)
registerTraceClass `Meta.isDefEq.assign
registerTraceClass `Meta.isDefEq.assign.checkTypes (inherited := true)
registerTraceClass `Meta.isDefEq.assign.outOfScopeFVar (inherited := true)
registerTraceClass `Meta.isDefEq.assign.beforeMkLambda (inherited := true)
registerTraceClass `Meta.isDefEq.assign.typeError (inherited := true)
registerTraceClass `Meta.isDefEq.assign.occursCheck (inherited := true)
registerTraceClass `Meta.isDefEq.assign.readOnlyMVarWithBiggerLCtx (inherited := true)
registerTraceClass `Meta.isDefEq.eta.struct
end Lean.Meta