Kim Morrison 6f4bee8421 perf: avoid re-exporting Std.Time from grind_annotated (#11372) ... This PR makes the `Std.Time.Format` import in `Lean.Elab.Tactic.Grind.Annotated` private rather than public, preventing the entire `Std.Time` infrastructure (including timezone databases) from being re-exported through `import Lean`. The `grindAnnotatedExt` extension is kept private, with a new public accessor function `isGrindAnnotatedModule` exposed for use by `LibrarySuggestions.Basic`. This should address the +2.5% instruction increase on `import Lean` observed after merging #11332. 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude <noreply@anthropic.com>		2025-11-26 04:05:08 +00:00
..
bench	chore: add radar-based bench suite for stdlib (#11264)	2025-11-25 12:59:30 +00:00
bench-radar	chore: add radar-based bench suite for stdlib (#11264)	2025-11-25 12:59:30 +00:00
compiler	chore: rename String.ValidPos to String.Pos (#11240)	2025-11-24 16:40:21 +00:00
elabissues
ir
lake	chore: lake: update tests/toml (#11314)	2025-11-22 04:41:58 +00:00
lean	perf: avoid re-exporting Std.Time from grind_annotated (#11372)	2025-11-26 04:05:08 +00:00
pkg	feat: improve error message in the case of type class synthesis failure (#11245)	2025-11-21 21:24:27 +00:00
playground
plugin
simpperf
.gitignore
common.sh	chore: make workspaceSymbol benchmarks modules (#11094)	2025-11-05 18:40:39 +00:00
lakefile.toml
lean-toolchain