the ideal lambda syntax is
- λ x. e57.7%
- λ x, e4.9%
- λ x → e32.4%
- λ x λ e λ4.9%
142 votesFinal results
3
1
6
Conversation
One of Lean's syntactic idiosyncrasies is the use of a comma separator in lambdas and other binders. However, on a closer look we didn't really find any syntactic ambiguity when using a dot instead. So since we're thinking of doing a few basic syntax changes for Lean 4 anyway...
1
5
Assuming you've decided to start the expression with an actual λ, the Agda/Haskell arrow may be the most popular choice of a separator... but I find it hard to argue against the naturalness of the dot. And it may actually be ambiguous, which I guess is why Coq and Idris use =>.
4
3
