Zulip Chat Archive

Stream: general

Topic: lattice shortcuts


Floris van Doorn (Jun 27 2020 at 18:02):

As @Jeremy Avigad pointed out a while ago, it's a bit annoying to type lattice operations. I also noticed this. I made a PR to add a couple more leanprover/vscode-lean#194. After the PR there are 9 ways to input supr and infi and 4 ways to input sup and meet:
for supr: bigjoin, biglub, bigsqcup, bigsup, Sup, Join, Lub, Sqcup and supr
for sup: sup, join, lub and sqcup
dually for inf and infi

You now have to type inftyfor , supseteq for and bowtie (unused) for .

Floris van Doorn (Jun 27 2020 at 18:04):

I also changed \nin to mean \notin, that one got me a couple of times. There are some other changes, like \inter for \cap. Feel free to suggest others (and if people want, I'll also make this PR to Emacs mode).

Floris van Doorn (Jun 27 2020 at 20:50):

Currently \d and \i are for and . I would slightly prefer δ and ι. Opinions?

Alex J. Best (Jun 27 2020 at 21:36):

I'd agree but not strongly enough that I'd want to change if anyone was really unhappy.
For reference, δ is used 1200 times and ↓ only 20.
ι is 3000 times and ∩ 1000.
So \d seems like a no brainer, \i is closer and I'd imagine a lot of people are used to using \cap anyway for ∩.
While we're at it what about \t for τ . (and then could take \tr and \tri etc.). Its a bit more controversial I'm sure as is used 1405 times in mathlib and τ only 190, but it would start to make it more consistent: for a greek letter type \ and the first letter of its latin name.

Edward Ayers (Jun 27 2020 at 21:47):

I have a take on this:

        "tr": "◂", "tl" : "▸",                           "tu" : "▾", "td" : "▴",
        "lr": "<", "ll" : ">", "lre" : "≤", "lle" : "≥", "lu" : "∨", "ld" : "∧", "luu": "⋁", "ldd": "⋀",
        "sr": "⊏", "sl" : "⊐", "sre" : "⊑", "sle" : "⊒", "su" : "⊔", "sd" : "⊓", "suu": "⨆", "sdd": "⨅",
        "cr": "⊂", "cl" : "⊃", "cre" : "⊆", "cle" : "⊇", "cu" : "∪", "cd" : "∩", "cuu": "⋃", "cdd": "⋂",
        "ir": "⊲", "il" : "⊳", "ire" : "⊴", "ile" : "⊵", "iu" : "∇", "id" : "∆",
        "vr": "≺", "vl" : "≻", "vre" : "≼", "vle" : "≽", "vu" : "⋎", "vd" : "⋏",

Alex J. Best (Jun 27 2020 at 21:55):

Wow, I think your left/rightness of triangles convention is the opposite of tex's though!

Edward Ayers (Jun 27 2020 at 22:10):

Ah man I've been reading triangles wrong my whole life!

Mario Carneiro (Jun 28 2020 at 03:01):

how does this convention interact with \l for lambda vs left arrow?

Johan Commelin (Jun 28 2020 at 04:04):

left arrow should of course be \al, and then there will also be \ar and \ad and \au.

Johan Commelin (Jun 28 2020 at 04:05):

I think \lam and \lef both occur often enough that we can switch \l to lambda. Reprogramming the muscle memory will only take 37 days.

Jeremy Avigad (Jun 28 2020 at 13:30):

When this settles, I'll update the text of MiL to include the new lattice shortcuts.

Edward Ayers (Jun 29 2020 at 10:56):

Mario Carneiro said:

how does this convention interact with \l for lambda vs left arrow?

        "-r"  : "→", "-l"  : "←", "-u"  : "↑", "-d"  : "↓", "-lr" : "↔", "-ud": "↕", "-rr" : "⟶", "-ll" : "⟵",
        "mtr" : "↦", "mtl" : "↤", "mtu" : "↥", "mtd" : "↧",
        "epl" : "↞", "epr" : "↠", "epu" : "↟", "epd" : "↡",
        "hpl" : "↩", "hpr" : "↪",              "hpd" : "↷",
        "ltr" : "↝", "ltl" : "↜",
        "mol" : "↢", "mor" : "↣",
        "=l" : "⇐", "=u"  : "⇑", "=r" :  "⇒", "=d" :  "⇓", "=lr" : "⇔", "=ud" : "⇕",
        "=ul" : "⇖", "=ur" : "⇗", "=dr" : "⇘", "=dl" : "⇙",
        "fl" : "⥢", "fr": "⥤", "fu": "⥣", "fd": "⥥",
        "hlu" : "↼", "hru": "⇀", "hur" : "↾", "hdr" : "⇂", "hld" : "↽", "hul" : "↿",  "hrd" : "⇁",  "hdl" : "⇃",
        "zr" : "⇝", "zl" : "⇜", "zlr" : "↭", "zd" : "↯", "zrr" : "⟿",

Edward Ayers (Jun 29 2020 at 10:59):

        "al": "α", "be": "β", "ga": "γ", "de": "δ", "ep": "ε", "ze": "ζ",
        "et": "η", "th": "θ", "io": "ι", "ka": "κ", "la": "λ", "mu": "μ",
        "nu": "ν", "xi": "ξ", "pi": "π", "rh": "ρ", "si": "σ",
        "ta": "τ", "ph": "φ", "ch": "χ", "ps": "ψ", "om": "ω",

Last updated: Dec 20 2023 at 11:08 UTC