dot notation with implicit args

Stream: mathlib4

[Yury G. Kudryashov]

Is it intentional that in Lean 4 the following works?

theorem List.tmp {l : List ℕ} (a : ℕ) : l = a :: [] → True := fun _ => trivial

example : True := by
  have h := [1].tmp
  exact h 1 rfl

[Yury G. Kudryashov]

See docs4#Multiset.erase_add_left_pos for a real-world example.

[Yury G. Kudryashov]

In Lean 3, t.erase_add_left_pos used t for the first explicit argument. In Lean 4, it uses t for the first implicit argument.

[Kyle Miller]

Here's an issue related to this, but with how its using implicit arguments interacts with dot notation for pi types.

[Reid Barton]

The new behavior is much nicer when it comes to instances, because you can just project out of them as though they were structures.