Where can I find a list of all symbols (and their meaning)?

Stream: new members

[Filippo Cozzi]

searching on the internet lean symbols doesn't result in much, and I can't seem to find information like this on lean community or in the language reference or anywhere else. Am I missing some important resources?

[Julian Berman]

Are you looking for information on how to type things? If so you can hover over a symbol and it will tell you how to type it -- or if you type Cmd+Shift+P in VSCode to open the command palette and then search for "Lean 4 Docs: Show Unicode Input Abbreviations" it will give you a big list.

If you're instead looking for what symbols are used for in Mathlib, I don't think there is such a big list of every notation yet, but the easiest way is to again have one in front of you and then hover over it, or use go to definition, and you'll see what it is being used for.

[Filippo Cozzi]

how does it work in lean.nvim?

[Julian Berman]

In lean.nvim you can use <localleader>\ on top of a symbol and it will tell you how to type it, or you can use :Telescope lean_abbreviations to search through them with telescope.

(From a "what's available" standpoint we use the same exact file as VScode)

[Julian Berman]

(If you've never used <localleader> before, the default is \, so that would be \\ on top of any unicode symbol)

[Filippo Cozzi]

thanks. Can <localleader> be remapped to <leader>?

[Julian Berman]

You can set it to whatever you'd like, I have mine set to <leader><leader> (and my leader is space): https://github.com/Julian/dotfiles/blob/main/.config/nvim/init.lua#L3-L4

[Jakub Nowak]

iirc, you have the enable mappings in the config for the <localleader>\ mapping to be avaiable. It's disabled by default.