Implicit arguments after explicit arguments

Stream: lean4

[Yury G. Kudryashov]

Is it intentional that I have to use _k _n in the first example but not in the second one?

example : ∀ {m : Nat}, 0 < m → ∀ {k n : Nat}, m < k → k < n → 0 < n := fun hm _k _n hk hn ↦
  Nat.lt_trans hm <| Nat.lt_trans hk hn

example : ∀ {m : Nat}, 0 < m → ∀ {k n : Nat}, m < k → k < n → 0 < n := fun hm ↦ fun hk hn ↦
  Nat.lt_trans hm <| Nat.lt_trans hk hn

[Jireh Loreaux]

sorry, what's the difference there?

[Yury G. Kudryashov]

In the first example I use one fun, then Lean hides m from fun but I have to use _k _n. In the second example, I use two funs, no _k _n.

[Jireh Loreaux]

oh sorry, I was looking at the statements. got it.

[Yury G. Kudryashov]

So, is it a bug or a feature? Is it documented somewhere?

[Eric Wieser]

This looks like a feature to me

[Mario Carneiro]

not to me, it is inconsistent with the implicitness of the arguments passed to the function - you would have to write _example hm hk hn as equivalent to @_example _ hm _ _ hk hn

[Yury G. Kudryashov]

So, should I open a Lean 4 github issue?

[Eric Wieser]

Oh, is your claim that the first line is misbehaving, Mario?

[Yury G. Kudryashov]

I think that it should be either changed to require fun hm hk hn in the first line or should be clearly documented (and the inconsistency with application syntax should be explained somehow).

[Ruben Van de Velde]

Somewhat related: if you do fun a => ..., lean happily introduces any implicit arguments before a, but if you want to abstract over only implicit arguments, you need fun {...}

[Yury G. Kudryashov]

Can't you just omit fun => in this case?