Gabriel Ebner

> The main issue here is performance. If we allow type class resolution > to invoke arbitrary tactics, then all caching infrastructure will have to be disabled. If I see...

I have just implemented feature request number one. (Apply to-function and to-sort coercion in function arguments.) For completeness, I'd like to add the following feature request as well: to-function coercions...

Ok, as far as I can tell there are 3 separate issues here: 1. Hover and go-to-definition in error messages. IMHO this mostly depends on structured error/trace messages as in...

> On the slack channel, we also discussed the possibility of adding "purge" messages from editor to server. [..] this would complicate the editor side. We only need to do...

> However, terms as formats would complicate position computations and seems to conflict with the idea of returning them as syntax. Once we implement both #1692 and #1674, we can...

> [Once we implement both #1692 and #1674, we can just add a message.from_syntax case.] Wouldn't that still be a static (text width-independent) layout? I really don't know how we...

> This is an issue when using Lean in an editor such as Emacs and VS Code, and we want to see the effect of our tactics (i.e., the resulting...

I think this is a good approach. ASTs that are close to the source code are pretty popular these days. Scala's meta-programming framework also recently switched to it (scala.meta). >...

> The syntax object will also represent faithfully constructs such as match-exprs, do-blocks, calc-blocks, etc which are currently expanded at parsing time. Notation should probably also remain unexpanded then.

> Fundamentally, though, infix operators are a feature of read, and read is responsible for handling them. Maybe infix operators were a bit of red herring. What I was wondering...