In Haskell I can use parentheses to convert an infix operator like + into a prefix function so (+) 2 3 is the same as 2 + 3. Is there a similar feature in Lean?
Is there a prefix notation in Lean?
Viewed 99
1 Answers
In Lean 4 there is the new · "this is a placeholder for a function input" notation, so you can do cool things like
#check (· + 1)
-- fun a => a + 1
#check (2 - ·)
-- fun a => 2 - a
#eval [1, 2, 3, 4, 5].foldl (·*·) 1
-- 120
(these examples from the manual). In Lean 3 you can use the Haskell trick: #eval (+) 2 3 returns 5.
Related