compilation error when trying to define a new python like pow operator

Viewed 49

I want to mimic the Python's infix operator ** in Idris2:

(**) : Double -> Double -> Double
(**) x y = pow x y 

But I'm getting this error:

Error: Couldn't parse declaration.

What am I doing wrong?

0 Answers
Related