Notation

Stream: general

[Billy Price]

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]

they are all magic pieces of syntax of the notation command

[Floris van Doorn]

They are just keywords for the notation command. They have no meaning in Lean.

[Mario Carneiro]

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]

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]

Also scoped and binders

[Billy Price]

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

[Mario Carneiro]

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]

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]

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

[Yury G. Kudryashov]

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]

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]

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