lean4-htt/tests
Kim Morrison 157fbd08b4
feat: set_library_suggestions makes auxiliary def, rather than storing Syntax (#11396)
This PR changes `set_library_suggestions` to create an auxiliary
definition marked with `@[library_suggestions]`, rather than storing
`Syntax` directly in the environment extension. This enables better
persistence and consistency of library suggestions across modules.

The change requires a stage0 update before tests can be restored. After
CI updates stage0, a follow-up PR will restore the test cases.

🤖 Generated with [Claude Code](https://claude.com/claude-code)
2025-11-28 04:36:31 +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 feat: set_library_suggestions makes auxiliary def, rather than storing Syntax (#11396) 2025-11-28 04:36:31 +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
lakefile.toml
lean-toolchain