Mario Carneiro

Also relevant: the issue only happens when the two variables are named the same. If the second identifier is named `y`, they are both highlighted independently and go to definition...

I'm dubious about `{! !}`, because we had that in lean 3 and it essentially didn't get used at all. I think it needs a proper retrospective to figure out...

It seems to be difficult to reproduce. If you just make a copy of `MetavarContext.lean`, inside or outside the lean4 repo, then the hovers work fine. It might be some...

I'm going to be making an in depth pass over everything in the coming weeks, so I'll keep an eye out for dot-notation candidates. But I don't have any suggestions...

> > Let-values in programming contexts. (See also Mario's let dep proposal in #1345) > > I like the `let dep` proposal, but we should probably get support from users...

Regarding using the `nonDep` flag: I was actually thinking the other way around: we would rename `let_fun` to `let` and `let` to something else, so `let` syntax would normally desugar...

`letD` is short and reminiscent of `letI` from mathlib which was used in the instance use-case (no longer needed in lean 4)...?

Is it feasible to use command keywords here: `def` for `let dep` and `abbrev` for `let inline`?

Regarding let_fun verbosity: although I think that's a good argument for why to use `letE`, I think that also points to the need to have a telescope operator for handling...

This code (in the PR) has the same performance as the `union` approach for `get_unchecked`, but if the implementation actually used `union` this would affect the ability to have regular...