da62a81e5e
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). |
||
|---|---|---|
| .. | ||
| UserAttr | ||
| lakefile.lean | ||
| lean-toolchain | ||
| test.sh | ||
| UserAttr.lean | ||