Def Lean.Elab.InfoTree.getTheorems

Modification history

2025-11-25 19:25
Mathlib/Lean/Elab/InfoTree.lean
feat(Linter): port unused `Decidable*` instance hypothesis linter (#31142) …
Added Lean.Elab.InfoTree.getTheoremsView on Github →