在Lean中有前缀符号吗？

Question

在Haskell中，我可以使用括号将+等中缀运算符转换为前缀函数，因此(+) 2 3与2 + 3相同。在Lean中有类似的特性吗？

Answer 1

在Lean4中，有了新的·“这是一个函数输入的占位符”符号，所以你可以做一些很酷的事情，比如

#check (· + 1)
-- fun a => a + 1
#check (2 - ·)
-- fun a => 2 - a
#eval [1, 2, 3, 4, 5].foldl (·*·) 1
-- 120

(这些来自the manual的示例)。在精益3中，你可以使用Haskell技巧：#eval (+) 2 3返回5。