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). |
||
|---|---|---|
| .. | ||
| bench | ||
| bench-radar | ||
| compiler | ||
| elabissues | ||
| ir | ||
| lake | ||
| lean | ||
| pkg | ||
| playground | ||
| plugin | ||
| simpperf | ||
| .gitignore | ||
| CMakeLists.txt | ||
| common.sh | ||
| lakefile.toml | ||
| lean-toolchain | ||