max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/src/Lean/Language
History
Sebastian Ullrich 96f9ee2a41
feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457) 
This PR ensures info tree users such as linters and request handlers
have access to info subtrees created by async elab task by introducing
API to leave holes filled by such tasks.

**Breaking change**: other metaprogramming users of
`Command.State.infoState` may need to call `InfoState.substituteLazy` on
it manually to fill all holes.
2025-03-13 15:09:00 +00:00
..
Lean feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457) 2025-03-13 15:09:00 +00:00
Basic.lean feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366) 2025-03-07 13:50:56 +00:00
Lean.lean feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457) 2025-03-13 15:09:00 +00:00
Util.lean feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366) 2025-03-07 13:50:56 +00:00