Sebastian Ullrich da62a81e5e feat: shake: track simpset/grindset uses (#12375) ... This PR extends shake with tracking of attribute names passed to `simp`/`grind`. On the way there, it also fixes `register_simp/grind_attr` uses outside `public meta section` as well as go-to-definition on declaration-level uses of the created attributes (tactic-level goto would be a separate todo).		2026-02-07 15:19:15 +00:00
..
BlaAttr.lean	feat: shake: track simpset/grindset uses (#12375)	2026-02-07 15:19:15 +00:00
Tst.lean	feat: shake: track simpset/grindset uses (#12375)	2026-02-07 15:19:15 +00:00