search

leanprover / vscode-lean

Extension for VS Code that provides support for the older Lean 3 language. Succeeded by vscode-lean4 ('lean4' in the extensions menu) for the Lean 4 language.
Apache License 2.0
116 stars 49 forks source link

Correct the symbol for perpendicular #328

Closed eric-wieser closed 1 year ago

eric-wieser commented 1 year ago

Unicode has two separate symbols for "up tack" (ie has_bot.bot) and "perpendicular" (not yet used in mathlib). Having \perp produce the former is confusing.

gebner commented 1 year ago

Note that we already heavily use ⊥ in mathlib (and not ⟂). For such a change I would like to see a consensus on zulip, and a commitment to a transition plan in both mathlib3 and mathlib4.

Because as soon as we release this change, people will rightfully complain that \perp no longer works.

gebner commented 1 year ago

We don't use ⊥ just for bottom elements. We also use the character for some orthogonality relations, like mutually singular measures.

eric-wieser commented 1 year ago

I've created a Zulip thread. Thanks for finding the other uses!

eric-wieser commented 1 year ago

Zulip consensus is unanimous; I don't think there's any lean 4 consideration here besides updating the abbreviations for that extension too; and I suspect we are already out of sync there.