feat: expose fields required for implementing linters outside of Lean core with detailed auto-fixes and diagnostic tags #13610

wvhulle wants to merge 4 commits intoleanprover:masterleanprover/lean4:masterfrom

wvhulle:message-diagnostic-fieldswvhulle/pretty-lean:message-diagnostic-fieldsCopy head branch name to clipboard