Make clearer the difference between what x is in (x), {x}, or {{x}} versus in [x].

[nielsvoss]

Describe the error

In 3.2.1.3. Implicit Functions:

Arguments for instance implicit parameters are found via type class synthesis. Instance implicit parameters are written in square brackets ([ and ]), and in most cases omit the parameter name because instances synthesized as parameters to functions are already available in the functions' bodies, even without being named explicitly.

Why is it incorrect and/or confusing?

This isn't actually a mistake, but I think it wasn't properly emphasized that the presence of a single term in () and {} is different from the presence of a single term in []. In (x), x is an identifier name, whereas in [x], x is a type. This can technically be seen in the Function Binders section, but maybe it could be better emphasized.

It might also be worth mentioning that while (x y : Nat) is legal, [x y : SomeTypeclass] is not.

As a side note: The section is called "Implicit Functions" right now, but maybe "Implicit Parameters" would be a better name.

[david-christiansen]

Thank you, this is very useful feedback. I agree about the section name.