12 ms·
thank you for explaining, but do i need a special keyboard just to type out the natural number type?
by prisonguard 3y ago
thank you for explaining, but do i need a special keyboard just to type out the natural number type?
- nodogoto 3y agoNo, you just type \N. You can also use `nat` instead if you prefer.
- deadbeef57 3y agoNo, you can just type `\nat` and the Lean extension in VScode will turn it into `ℕ`. Similarly, you can type many LaTeX macros, and the will render in unicode. Examples: `\times` becomes `×` and `\to` becomes `→`, etc...