Parameters with infix operator name?

Viewed 44

In Haskell, we can use an infix operator as a parameter name, e.g.:

f :: (Int -> Int -> Int) -> Int
f (|+|) = 3 |+| 4

Is it possible to do something similar in Idris 2? I tried the following:

f : (Int -> Int -> Int) -> Int
f (|+|) = 3 |+| 4

But it fails with:

 Unknown operator '|+|'
 
 slice:2:11--2:18
  1 | f : (Int -> Int -> Int) -> Int
  2 | f (|+|) = 3 |+| 5
                ^^^^^^^
0 Answers
Related