How to declare functions with infix style in Idris

Question

The non infix example works:

myelem: (Eq a) => a -> List a -> Bool
myelem x []     = False
myelem x (y::ys) = x == y || (myelem x ys)

I've tried another permutation fo the following, where I remove the backticks from the type declaration line, but either way it fails:

`myelem`: (Eq a) => a -> List a -> Bool
x `myelem` []     = False
x `myelem` (y::ys) = x == y || (x `myelem` ys)

This is using Idris 1.3.0

Answer 1

You only use the backticks on the usage site, not on the declaration site:

myelem: (Eq a) => a -> List a -> Bool 
myelem x []     = False
myelem x (y::ys) = x == y || (x `myelem` ys)

There is no way (I know of) to use infix syntax on the declaration site for the function you are just about to define.

Edit: There is however a way to do what you want with infix functions in the bracket notation. The example is taken from the Prelude:

infixr 4 <$>
(<$>) : Functor f => (func : a -> b) -> f a -> f b
func <$> x = map func x