Zulip Chat Archive

Stream: general

Topic: VSCode allm


view this post on Zulip Patrick Massot (Aug 24 2020 at 15:22):

Did the shortcut for the almost everywhere quantifier changed recently? VSCode has a translation allm that sounds like it should produce this symbol but misplaces the m (subscript instead of superscript). Or is this meant to be something completely different?

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:22):

@Yury G. Kudryashov

view this post on Zulip Gabriel Ebner (Aug 24 2020 at 15:22):

I think @Floris van Doorn changed this recently.

view this post on Zulip Gabriel Ebner (Aug 24 2020 at 15:23):

Recently = February: https://github.com/leanprover/vscode-lean/pull/141

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:24):

Thanks, but I'm looking for a change in measure theory, to make sure this was the intended use of this translation.

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:28):

https://github.com/leanprover-community/mathlib/commit/7d31f772496b484294b74b3cfb3717ea4a519799#diff-f741d98d7d24ed2ccdae58f7795e25e1R1030

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:28):

I found it.

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:29):

- notation `∀ₘ` binders `∂` μ `, ` r:(scoped P, μ.ae.eventually P) := r
+ notation `∀ᵐ` binders `∂` μ `, ` r:(scoped P, μ.ae.eventually P) := r

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:30):

So I think I can open a translation PR.

view this post on Zulip Patrick Massot (Aug 24 2020 at 15:32):

https://github.com/leanprover/vscode-lean/pull/224 (no hurry at all to release that)

view this post on Zulip Patrick Massot (Aug 24 2020 at 16:09):

Thanks Gabriel!


Last updated: May 18 2021 at 15:14 UTC