Samuel
@samuel.fm
do people who work on advanced type systems have special keyboards or something or do they google for "weird rounded e unicode" every time
18 1 66
dan
for me, neither! in Lean, this comes by default with their VS Code extension. i got used to it on the first day \to gives you an arrow \all gives you “for all” \exists gives you “exists” \a gives you alpha \e gives you epsilon (iirc) and so on. also each symbol has a hover telling you the combo
4 20
dan
the only times i realize the whole world doesn’t work like this is when i try to type in the browser and it doesn’t do that. so i open vs code, type there and then copy paste
1 4
Jeff Silksong Coelho
(Yes, I realize that those lean shortcuts mentioned are not latex compatible unless you define the proper latex macro \a etc to alias to \alpha, and some differences too, but all are workable)
1 2
dan
yes i actually appreciate it’s not latex because i’ll just never learn latex
1 1
dan
but iirc Lean shortcuts support latex too. they have more than one shortcut per symbol. sometimes three
2
Andrea
owwwwww this is different from LaTeX but uses the same \ and my brain hurts just hearing about it
1 3
dan
haha yeah but i think it supports latex too, it just has several shortcuts for each symbol
3
Metaflame
huh wdym, I got myself a special academic keyboard just to be able to type those fancy math symbols it cost me €10000 (incl. VAT) to get started with Lean because of that & my room now looks like an aircraft cockpit, so I HOPE it'll be worth it (/j ofc)
1 1
Andj C
I found it easier to just create a custom keyboard layout that was able to input everything I usually need.
chelsea bridge
the secret is that they never actually make anything with their languages so they never have to type the weird e hee hee
2 10
Catherine Frames
I imagine they have editor plugins for it. every Julialang editor plug in makes backslash then the character name tab complete to convent to the unicode characters.
2
Myoukochou
See what you can do is use AutoHotKey to give yourself way more and customised AltGr+ shortcuts. That’s what I do, anyways.
3
a bezoar
The Yoneda embedding is a very important concept in category theory. Some authors spell that functor as "よ".
2
Ian
Use something like Espanso - can define in it little character sequences to be replaced as you type them with something else, like an awkward character
1
Michael Rutter
IDE integrations and there is some commonality between what these symbols are called in latex and other markup tools. So if you're working in the domain, these completions and names for things are pretty common. \forall in latex is forall in other domains, which typically gets rendered as ∀.
Alona
according to friends, they use a vscode plugin (and copy/paste out of vscode if they want it elsewhere)