Referring to arguments by name or index

[herbelin]

First attempt at summarizing the situation about referring to arguments by name or index.

Rendered here.

[silene]

Here is my opinion on some of the choices:

• Given foo (A := bar) qux, qux is used to fill the first non-implicit argument that occurs after A. All the other arguments up to it are inferred (as if _), except for A obviously. Naming arguments in the wrong order is an error.
• As with with, an integer position should denote a dependent argument. (What is the actual rule? A dependent argument or an anonymous one?) No need for a syntax other than (3 := bar).
• No need for (id a := term). It feels too ugly and unintuitive to be worth it.
• No need for (fun A => A) (A:=nat). I am fine with the syntax being restricted to named symbols.

[herbelin]

As with with, an integer position should denote a dependent argument. (What is the actual rule? A dependent argument or an anonymous one?)

It is a non-dependent argument (which is what you meant I guess).

[silene]

Right. The terminology "(non) dependent" is always confusing me. It would be clearer if it was "non-depended-upon argument", but I guess that would be too much of a mouthful in practice.

[mattam82]

I think we should have a look at the stability criterion developed here: https://richarde.dev/papers/2021/stability/stability.pdf