syntax - 是否可以在 idris 的函数定义中使用守卫？

Question

在 haskell 中，可以这样写：

containsTen::Num a => Eq a => [a] -> Bool
containsTen (x : y : xs)
    | x + y == 10 = True
    | otherwise = False

是否可以在 Idris 中编写等效的东西，而不用ifThenElse（我的实际情况比上面的情况更复杂）？

Answer 1

Idris 没有与 haskell 完全相同的模式保护。有一个语法相似的with子句（但更强大，因为它支持存在依赖类型的匹配）：

containsTen : Num a => List a -> Bool
containsTen (x :: y :: xs) with (x + y)
    | 10 = True
    | _  = False

您可以查看Idris 教程第7 节视图和“with”规则。