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?

[Jovan Gerbscheid]

I ran into this issue as well:

example : True ↔ ∀ {α} (a : α), a = a :=
  ⟨fun _ => fun a => Eq.refl a, fun _ => trivial⟩

example : True ↔ ∀ {α} (a : α), a = a :=
  ⟨fun _ _ a => Eq.refl a, fun _ => trivial⟩

Note how fun _ => fun a => and fun _ _ a => are equivalent.
I find it weird that the {α} needs to be explicitly introduced if it's not the first argument in the fun.

[Kyle Miller]

What do you think would be less surprising? Options that come to mind:

• The body of fun could have implicit lambda disabled. This way, you would write fun _ => fun _ _ a => Eq.refl a.
• More drastically, fun binders could skip implicit parameters, and it it could require curly braces when implicit parameters need naming.

[Jovan Gerbscheid]

I would have expected the behaviour from point 2.

The way I think about it is that if {α} is at the start, then fun doesn't introduce it explicitly because the variable is marked to be implicit. And I would have expected this logic to apply to all introduced variables.

[Aaron Liu]

It's not that fun is skipping introducing the parameter, but that the implicit lambda feature is introducing this before propagating the expected type to the fun: compare

example : ∀ {n} (_ : 0 < n), 0 < n := fun hn => hn
example : ∀ {n} (_ : 0 < n), 0 < n := id

[Jovan Gerbscheid]

Ok, maybe a better way to argue is that I expect fun a => fun b => .. to do the same thing as fun a b => ..

[Jovan Gerbscheid]

Point 1 doesn't seem too bad either, because that also avoids this inconsistency. However I would have thought that point 1 would be the more drastic change of the two. (As in, there are more scenarios in which that change will become apparent)