Zulip Chat Archive

Stream: general

Topic: VSCode allm

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?

Patrick Massot (Aug 24 2020 at 15:22):

@Yury G. Kudryashov

Gabriel Ebner (Aug 24 2020 at 15:22):

I think @Floris van Doorn changed this recently.

Gabriel Ebner (Aug 24 2020 at 15:23):

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

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.

Patrick Massot (Aug 24 2020 at 15:28):

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

Patrick Massot (Aug 24 2020 at 15:28):

I found it.

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

Patrick Massot (Aug 24 2020 at 15:30):

So I think I can open a translation PR.

Patrick Massot (Aug 24 2020 at 15:32):

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

Patrick Massot (Aug 24 2020 at 16:09):

Thanks Gabriel!

Last updated: Dec 20 2023 at 11:08 UTC