feat(templates/glossary): explain dot notation

[Vierkantor]

As mentioned in #226.

[Julian]

Yay!

[robertylewis]

Suggested change

	Lean provides two interpretations of the syntax `foo.bar`: it can mean the declaration `bar` in the `foo` namespace, or it can be generalized field notation. Suppose `foo` has type `C x1 ... xn`, with `C` some constant and `x1 ... xn` arbitrary, then `foo.bar` is sugar for `C.bar foo`. For calls of the form `foo.bar _ ... _` with (implicit or explicit) arguments, Lean is smart enough to expand to `C.bar _ ... foo _ ... _`, so that everything typechecks. In these previous examples, `foo` can also be a more complicated expression such as function application.
	Lean provides two interpretations of the syntax `foo.bar`: it can mean the declaration `bar` in the `foo` namespace, or it can be generalized field notation. We expand here on the latter.
	Suppose `foo` has type `C x1 ... xn`, with `C` some constant and `x1 ... xn` arbitrary, and suppose that there is a declaration in the context named `C.bar` which takes an argument of type `C x1 ... xn`. Then `foo.bar` is sugar for `C.bar foo`. For calls of the form `foo.bar _ ... _` with (implicit or explicit) arguments, Lean is smart enough to expand to `C.bar _ ... foo _ ... _`, so that everything typechecks. In these previous examples, `foo` can also be a more complicated expression such as function application.

Tried to clarify slightly, since superficially it looks like we're defining dot notation in terms of dot notation.

I'm not sure what you mean by the final sentence "In these previous examples, foo can also be a more complicated expression such as function application."?

[Julian]

I think @Vierkantor was pointing out that (foo bar baz).quux also works, which I think is not a bad thing to point out; maybe just giving that full example will make it clearer.

[robertylewis]

@Vierkantor do you like these changes, and do you think @Julian 's suggestion to add an example of a "more complicated expression" would fit?

[Vierkantor]

Thanks for the reminder, I totally forgot about this PR!

How about:

Suggested change

	Lean provides two interpretations of the syntax `foo.bar`: it can mean the declaration `bar` in the `foo` namespace, or it can be generalized field notation. Suppose `foo` has type `C x1 ... xn`, with `C` some constant and `x1 ... xn` arbitrary, then `foo.bar` is sugar for `C.bar foo`. For calls of the form `foo.bar _ ... _` with (implicit or explicit) arguments, Lean is smart enough to expand to `C.bar _ ... foo _ ... _`, so that everything typechecks. In these previous examples, `foo` can also be a more complicated expression such as function application.
	Lean provides two interpretations of the syntax `foo.bar`: it can mean the declaration `bar` in the `foo` namespace, or it can be generalized field notation. We expand here on the latter.
	Suppose `foo` has type `C x1 ... xn`, with `C` some constant and `x1 ... xn` arbitrary, and suppose that there is a declaration in the context named `C.bar` which takes an argument of type `C x1 ... xn`. Then `foo.bar` is sugar for `C.bar foo`. For calls of the form `foo.bar _ ... _` with (implicit or explicit) arguments, Lean is smart enough to expand to `C.bar _ ... foo _ ... _`, so that everything typechecks. In these previous examples, `foo` can also be a more complicated expression such as the function application in `(foo bar baz).quux`.