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: Aug 03 2023 at 10:10 UTC