Robert J. Simmons d824f7e085 feat: identifier suggestions for non-dotted identifiers (#11619) ... This PR allows Lean to present suggestions based on `@[suggest_for]` annotations for unknown identifiers without internal dots. (The annotations in #11554 only gave suggestion for dotted identifiers like `Array.every`->`Array.all` and not for bare identifiers like `Result`->`Except` or `ℕ`->`Nat`.)		2025-12-11 19:47:18 +00:00
..
bench	feat: remove Finite conditions from iterator consumers relying on a new fixpoint combinator (#11038)	2025-12-08 16:03:22 +00:00
bench-radar	chore: measure dynamic symbols in benchmarks (#11568)	2025-12-11 16:10:27 +00:00
compiler	chore: minor String API improvements (#11439)	2025-12-01 11:44:14 +00:00
elabissues
ir
lake	chore: lake: mv targets test to tests (#11592)	2025-12-11 09:28:44 +00:00
lean	feat: identifier suggestions for non-dotted identifiers (#11619)	2025-12-11 19:47:18 +00:00
pkg	chore: switch the association of stored suggestions (#11590)	2025-12-10 21:42:05 +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