# Zulip Chat Archive

## Stream: general

### Topic: Notation

#### Billy Price (Jun 27 2020 at 04:42):

What "things" are `binders`

`foldr`

`scoped`

. I can't do `#check`

on any of them. Is `foldr`

different to `list.foldr`

- the usage looks different.

```
notation `[` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) := l
notation `∃!` binders `, ` r:(scoped P, exists_unique P) := r
```

#### Mario Carneiro (Jun 27 2020 at 04:45):

they are all magic pieces of syntax of the `notation`

command

#### Floris van Doorn (Jun 27 2020 at 04:45):

They are just keywords for the `notation`

command. They have no meaning in Lean.

#### Mario Carneiro (Jun 27 2020 at 04:45):

Even the `(h t, list.cons h t)`

isn't what it looks like - it's really more like `(\lam h t, list.cons h t)`

#### Billy Price (Jun 27 2020 at 04:50):

I see some mentions in the Lean reference manual on binders, but not much for foldr or foldl - is there documentation for them?

I am generally familiar with foldr and foldr, but it'd be nice to see docs on them.

#### Billy Price (Jun 27 2020 at 04:50):

Also scoped and binders

#### Billy Price (Jun 27 2020 at 04:50):

Actually I do understand what binders is, but not how it becomes related to the rest of the expression

#### Mario Carneiro (Jun 27 2020 at 09:54):

It's pretty much entirely pro forma. I don't think there are many reusable subparts of the `notation`

command, just those particular keywords in that order

#### Yury G. Kudryashov (Mar 03 2021 at 21:04):

I'm trying to add notation for a diffeomorphism between two normed spaces. Here is my code:

```
import geometry.manifold.diffeomorph
variables {𝕜 : Type*} [nondiscrete_normed_field 𝕜]
{E : Type*} [normed_group E] [normed_space 𝕜 E]
{E' : Type*} [normed_group E'] [normed_space 𝕜 E']
{H : Type*} [topological_space H]
{H' : Type*} [topological_space H']
(I : model_with_corners 𝕜 E H) (I' : model_with_corners 𝕜 E' H')
variables (M : Type*) [topological_space M] [charted_space H M] [smooth_manifold_with_corners I M]
(M' : Type*) [topological_space M'] [charted_space H' M'] [smooth_manifold_with_corners I' M']
(n : with_top ℕ)
namespace times_diffeomorph
notation E ` ≃ₘ^` n `[` 𝕜 `] ` E' := times_diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n
protected lemma times_cont_diff (h : E ≃ₘ^n[𝕜] E') : times_cont_diff 𝕜 n h := sorry
end times_diffeomorph
```

Lean fails to parse the lemma. What am I doing wrong? Does Lean assume that `[`

in the lemma is a part of `n`

?

#### Yury G. Kudryashov (Mar 03 2021 at 21:06):

I see that notation for docs#times_diffeomorph between two manifolds uses some fancy parentheses. Should I do the same?

#### Yury G. Kudryashov (Mar 03 2021 at 21:06):

If yes, how do I disambiguate new and old notation? Here is the existing notation:

```
localized "notation M ` ≃ₘ^ `n `⟮` I `,` J `⟯` N := times_diffeomorph I J M N n" in manifold
localized "notation M ` ≃ₘ⟮` I `,` J `⟯` N := times_diffeomorph I J M N ⊤" in manifold
```

#### Yury G. Kudryashov (Mar 03 2021 at 21:08):

UPD: this works:

```
notation E ` ≃ₘ^` n:1000 `[`:50 𝕜 `] ` E' := times_diffeomorph (model_with_corners_self 𝕜 E) (model_with_corners_self 𝕜 E') E E' n
```

#### Yury G. Kudryashov (Mar 03 2021 at 21:09):

What are the policies about priorities? What should I use instead of 1000 and 50?

Last updated: May 06 2021 at 22:13 UTC