是否可以在idris的函數定義中使用警衛？

Question

在Haskell，一個可以寫：

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

是否有可能寫的東西相當於伊德里斯，而不ifThenElse做（我的實際情況比上面的一個更復雜的）？

Answer 1

伊德里斯沒有像哈斯克爾一樣的模式守衛。有與條款，在語法上是相似的（但功能更強大，因爲它支持依賴類型存在匹配）：

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

你可以看看Idris tutorial部分7次和「與」規則。