如何在 Idris 中使用中缀样式声明函数

Question

非中缀示例有效：

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

我尝试了以下另一种排列，其中我从类型声明行中删除了反引号，但无论哪种方式都失败了：

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

这是使用 Idris 1.3.0

Answer 1

您仅在使用站点上使用反引号，而不是在声明站点上使用反引号：

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

（据我所知）无法在您即将定义的函数的声明站点上使用中缀语法。

编辑： 但是，有一种方法可以使用括号表示法中的中缀函数来完成您想要的操作。该示例取自Prelude：

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