Zulip Chat Archive

Stream: general

Topic: Notation


view this post on Zulip 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

view this post on Zulip Mario Carneiro (Jun 27 2020 at 04:45):

they are all magic pieces of syntax of the notation command

view this post on Zulip Floris van Doorn (Jun 27 2020 at 04:45):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip Billy Price (Jun 27 2020 at 04:50):

Also scoped and binders

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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