时间戳

首页 > 解决方案 > 如何在 Idris 中声明具有中缀样式的函数

idris - 如何在 Idris 中声明具有中缀样式的函数

问题描述

非中缀示例有效：

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

标签： idris

解决方案

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

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

推荐阅读