What question should the reference manual answer?
We have a section on generalized field notation, but it took me a while to find it, because I was searching for the term "extended field notation", which we also use, for example here in the source code: https://github.com/leanprover/lean4/blob/4786e082dca22873d14d2a5b9b7c8843380c6e78/src/Lean/Parser/Term.lean#L836.
It would be cool if putting "extended field notation" into the search box found https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#generalized-field-notation.
What question should the reference manual answer?
We have a section on generalized field notation, but it took me a while to find it, because I was searching for the term "extended field notation", which we also use, for example here in the source code: https://github.com/leanprover/lean4/blob/4786e082dca22873d14d2a5b9b7c8843380c6e78/src/Lean/Parser/Term.lean#L836.
It would be cool if putting "extended field notation" into the search box found https://lean-lang.org/doc/reference/latest/Terms/Function-Application/#generalized-field-notation.