operators - 精益中有前缀符号吗？

Question

在 Haskell 中，我可以使用括号将中缀运算符 like+转换为前缀函数，因此(+) 2 3与2 + 3. 精益中是否有类似的功能？

标签： operatorslean

Answer 1

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

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

（这些示例来自手册）。在精益 3 中，您可以使用 Haskell 技巧：#eval (+) 2 3返回 5。