Sebastian Ullrich

The current name resolver is a bit of a mess and duplicated across parser and elaborator. I don't think we'll want to touch it before it is replaced in the...

There is no such tool yet. However, the next version of Lean, Lean 4, will provide users with access to a concrete syntax tree representation of Lean code, which should...

I'm not quite sure what you mean. `String` eagerly, always caches the number of code points.

Note: we should double-check to not compile-time evaluate any values dependent on `getIsWindows` and similar functions.

FWIW, I think the LSP comment should be restated to point out that this is only a problem with clients without (correct) `PublishDiagnosticsClientCapabilities.versionSupport?`. Which I'd very much hope is none...

Yikes, I assumed that they would at least ignore diagnostics with regressing version numbers... I only checked that lsp-mode set `versionSupport` to `t`, but it doesn't look like it does...

This is even more important after #941. Instead of ``` @Option.none.{?u.1345} : {α : Type ?u.1345} → Option α ``` we really should be printing ``` Option.none.{u} {α : Type...

@Vtec234 We probably want to make sure that the output is still usable as an interactive message for widgets, correct? That is, even if the LSP hover is currently non-interactive,...

A signature is not a valid term syntax, so this can't be part of the delaborator unconditionally. In theory, we could introduce a purely internal delaborator option for formatting a...

OTOH, I'm not even sure we want to use the signature printer on `#check none` since `#check` takes terms in general, not single idents. So this might be a mostly...