是否可以在 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 tutorial 部分7 Views 和“with”规则。