idris - 尝试定义新的 Python （如 pow 运算符）时出现编译错误
问题描述
我想**在 Idris2 中模仿 Python 的中缀运算符：
(**) : Double -> Double -> Double
(**) x y = pow x y
但我收到了这个错误：
Error: Couldn't parse declaration.
我究竟做错了什么？
我想**在 Idris2 中模仿 Python 的中缀运算符：
(**) : Double -> Double -> Double
(**) x y = pow x y
但我收到了这个错误：
Error: Couldn't parse declaration.
我究竟做错了什么？
标签： idris