4

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?

eyelash
  • 3,197
  • 25
  • 33

1 Answers1

6

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.

Kevin Buzzard
  • 374
  • 1
  • 4
  • 2
    It might be worth mentioning that a regular ASCII period `.` can also be used as an alternative to this Unicode symbol. – eyelash Jun 23 '21 at 09:17