Zulip Chat Archive

Stream: general

Topic: lattice shortcuts


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

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

view this post on Zulip Floris van Doorn (Jun 27 2020 at 20:50):

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

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

view this post on Zulip 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" : "⋏",

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

view this post on Zulip Edward Ayers (Jun 27 2020 at 22:10):

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

view this post on Zulip Mario Carneiro (Jun 28 2020 at 03:01):

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

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

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

view this post on Zulip Jeremy Avigad (Jun 28 2020 at 13:30):

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

view this post on Zulip 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" : "⟿",

view this post on Zulip 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: May 15 2021 at 00:39 UTC