Lean中有前缀表示法吗？

Question

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

Answer 1

在 Lean 4 中，有新的\xc2\xb7“这是函数输入的占位符”符号，因此您可以做一些很酷的事情，例如

\n

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

\n

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

\n