newbee question about fn application

Stream: new members

[csmoe]

I cannot find a channel for lean4 newbee, really sorry for disturbing here.

while reading functional programming in lean to learn lean4, these sentences confused me a lot:
image.png

Because the remaining arguments are not explicitly named, no further substitution occurs as more arguments are provided

where does the substitution stop as no further substitution?

[Notification Bot]

This topic was moved here from #general > newbee question about fn application by Eric Wieser.

[Scott Morrison]

(The new members stream, where Eric has moved your question, @csmoe, is perfect for new user questions, whether for Lean 3 or Lean 4.)

[Scott Morrison]

That's not how I would have worded that sentence, and I agree it doesn't make much sense as written.

[Scott Morrison]

I think it is meant to mean "since the remaining arguments are no longer dependent on each other, no further substitutions will occur as more arguments are provided".

[Scott Morrison]

I guess it does make sense as written: #check is only going to show an argument as having a name, if later arguments have types depending on that argument.

[Scott Morrison]

The confusing part is that he's talking about "having an explicit name", which is really just about how #check prints things, rather than the fundamental property of whether it is a dependent function or not.

[csmoe]

thanks :smile: