是否可以在idris的函数定义中使用保护？

Question

在haskell,人们可以写:

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

是否有可能在伊德里斯写一些相同的东西,而不用它ifThenElse(我的真实案例比上面的更复杂)？

Answer 1

伊德里斯没有完全像haskell那样的模式保护.有一个with子句在语法上相似(但更强大,因为它支持在依赖类型的存在下匹配):

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

您可以查看Idris教程第7节视图和"with"规则.