Gabriel Ebner

Can you explain what's going wrong in the example above? Is it too much indentation? I'm not completely happy with the `ppAllowUngrouped` solution either.

We want to make string interpolation the default anyhow: #407

:+1: for the go-to-instance feature, this is often requested. > while go-to-declaration should go to the typeclass as it does right now Actually, I think it goes to the notation....

I didn't look through the implementation yet, but I love the semantics! Finally a `wlog` that I understand and that works like a w.l.o.g. on paper! What is the reason...

@jcommelin Do you have concrete examples for the mysterious behavior? You said something about `generalize` on zulip. Everything seems to build here though.

> The difference between completions and code actions seems to be that code actions are present as solutions to diagnostics ('squigglies'), This is not accurate. Code actions are not usually...

Typescript does AST modification: - Example code action: https://github.com/microsoft/TypeScript/blob/7910c509c4545517489d6264571bb6c05248fb4a/src/services/codefixes/addMissingAsync.ts#L48-L62 - Some high level docs: https://github.com/microsoft/TypeScript/wiki/Codebase-Services-TextChanges

See also #1510.

> During code specialization, monomorphise `ptrEq`. I like this approach. It also helps with decidability instances for polymorphic types: ```lean instance [DecidableEq α] : DecidableEq (List α) := ... ```...

We could define `PNonScalar` using choice. This 1) makes it explicitly an unspecified type, 2) works with both the old and new compiler (being erased to the any type as...