From 290141908f5ca41e3df56d66c0d6a3f31c3280db Mon Sep 17 00:00:00 2001 From: Anne Baanen Date: Mon, 22 Nov 2021 14:00:36 +0000 Subject: [PATCH] feat(templates/glossary): explain dot notation As mentioned in #226. --- templates/glossary.md | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/templates/glossary.md b/templates/glossary.md index 6e4b294e55..9cca64e64c 100644 --- a/templates/glossary.md +++ b/templates/glossary.md @@ -149,6 +149,12 @@ Diamonds which cross library boundaries -- such as ones in which part of the typ * [Forgetful Inheritance](https://leanprover-community.github.io/mathlib_docs/notes.html#forgetful%20inheritance), also from the mathlib documentation, for a discussion on a general pattern for avoiding diamonds in the case of "richer" and poorer structures on a type +### dot notation / generalized field notation / generalized projections + +The syntax sugar allowing notations such as `((foo a b c).bar x.y).baz`. + +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. + ### `equiv` As distinct from mathematical equality, [`equiv`](mathlib_docs/data/equiv/basic.html) allows for defining an equivalence or congruence of types.