Gabriel Ebner

Just mentioning this here because it came up on zulip. We could probably just resurrect the `haveI` and `letI` syntax in mathlib. Except that `I` is now short for "inline"...

> We had users complaining that let and haves were vanishing, and we fixed it. It seems some users would complain if we eagerly inline the haves. > For local...

> Any favorite bikeshed colors? I prefer colors that can be layered on top of each other and can be painted on many different surfaces. So it would be nice...

For reference, this is a working version of my proposal: ```lean import Lean open Lean Macro declare_syntax_cat lvalue /-- `lvalue ←% x => action` applies `action` to `lvalue`. In the...

Would it be an option to tag all nodes with the `info` generated from the reference?

> Aha, we do have some specific annotations for error positions such as in 01f8127. If we went with defaulting nodes to the ref range, those would get ignored Indeed,...

:+1: for the LSP logs. It would also be interesting to see what this prints on windows: ```lean #eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\Version.lean" #eval IO.FS.realPath "c:\\Temp\\vscode-lean4\\vscode-lean4\\test\\test-fixtures\\simple\\Test\\version.lean" ```

> I also don't immediately see a use case for this, but we could definitely consider it if one turns up. The obvious use case for the `Expr` version is...

> We have been trying to minimize the local context in error messages and the expected type info view. I know, that's why I'm trying to bring up particularly surprising...

> BTW, should we call it `let dep` or `let_dep`? I'd prefer `let dep` over `let_dep` (it fits in with `let mut`). I'm not sure I like the `dep` though...