Built-in operators and their precedence

[eyelash]

It's possible that I somehow missed it but I couldn't find a list of all the built-in operators (like +, -, %, <, etc.) with their relative precedence and associativity.

Here are some examples from other languages to get a better idea of what I'm looking for:

• C++
• C/C++ on Wikipedia
• JavaScript

I believe the list of operators for Lean can be found here.

[david-christiansen]

A table of operators is a bit more interesting in Lean, because the syntax is extensible. The set of available operators can depend on which libraries have been imported and which namespaces are opened.

That said, a table of all the operators that ship with Lean sounds useful.

In what concrete way would this help you get your work done?

[eyelash]

It doesn't necessarily have to be a table, just a single place where all the built-in operators are listed.

This would help me as follows:

When reading code, I might come across an expression such as 1 <<< 2 + 3 and I might wonder what <<< does or whether this expression is parsed as (1 <<< 2) + 3 or 1 <<< (2 + 3). Having a page in the reference manual where all the built-in operators are listed together with their precedence would allow me to quickly answer this question. Note that when I'm reading code I might not have access to IDE features such as go-to-definition since the code might be on GitHub or StackOverflow for example.

While writing code or learning the language, I want to know which operators are available at my disposal so that I can write my code in an optimal way. Having all the built-in operators listed in a single place would help me learn the language, especially since Lean is a functional language that comes with a few operators (>>=, >>, <*>, etc.) that might not be familiar to people coming from other languages.

The reference manual might not be the right place for such a list but having such a list somewhere would definitely be very helpful to me.

A table of operators is a bit more interesting in Lean, because the syntax is extensible. The set of available operators can depend on which libraries have been imported and which namespaces are opened.

It might be worth taking a look at the documentation for Swift, since it also allows you to define custom operators. Their documentation is split into two pages:

• Basic Operators explains what an operator is and then lists assignment (=, +=, etc.), arithmetic (+, *, etc.), comparison (==, <, etc.), logical (!, &&, ||), ternary conditional, nil-coalescing, and range operators.
• Advanced Operators explains bitwise and overflow operators, precedence and associativity, and how to create custom operators.

[david-christiansen]

That's very reasonable.

What about other syntax that isn't an infix, prefix, or postfix operator? For example, if... then... else... in Lean is equivalent to Swift's ternary conditional, which is on the page that you linked to, and the type ascription syntax has mandatory parentheses and thus is ( ... : ... ) rather than being an infix :. Would you be surprised if they were on such a list, or if they weren't?

I guess what I'm trying to tease out here is whether you would be best served by a table of operators per se, or rather by a table that lists all the different syntax that can be used to write terms, including operators, list/array literals, etc? It sounds to me like the latter is what you would find most valuable, so if you see #[1,2,3] you could look up #[ and see that it's part of the array syntax, or look up ] and see that it's part of list, array, and collection lookup syntax, or look up if and see that it's part of conditionals, pattern-matching conditionals, do-notation conditionals, and tactic conditional syntax. Is that a good understanding of your use case?

[eyelash]

Would you be surprised if they were on such a list, or if they weren't?

I wouldn't be surprised to find other syntax listed alongside operators but I also wouldn't be surprised if it wasn't.

For languages like JavaScript or C++ there is a relatively clear line between operators and other syntax, even though things such as the comma operator or parentheses used for grouping might already blur that line. The pages I linked above are already inconsistent in that regard. C++ also has the concept of operator overloading so it makes sense to list all the overloadable operators in one place. Given that Lean has a more extensible syntax and doesn't distinguish between expressions and statements it might actually make more sense to list all the built-in syntax instead of just the operators. I'm not very deep into Lean yet but the extensible syntax might raise the general question of how to look up a particular syntax or find out about all the available syntax, not just from the core language but also from libraries that define their own syntax.

For me personally, I'm mostly interested in a table of operators because they are hard to remember (since there are many of them) and they interact with each other through precedence. I'm unlikely to look up the if-then-else syntax because the English keywords already describe their meaning and precedence isn't very important here. For things such as #[] I would probably look in the chapters about lists and arrays. Also I would be surprised to find something like def or inductive on a page about operators.