Có thể sử dụng nhân viên bảo vệ trong định nghĩa chức năng trong idris không?

Question

Trong Haskell, người ta có thể viết:

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

Có thể viết một cái gì đó tương đương trong Idris, mà không làm nó với ifThenElse (trường hợp thật của tôi là phức tạp hơn so với cái ở trên)?

Answer 1

Idris không có bảo vệ mẫu chính xác như trong haskell. Có với khoản mà là cú pháp tương tự (nhưng mạnh hơn vì nó hỗ trợ tương ứng trong sự hiện diện của các loại phụ thuộc):

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

Bạn có thể có một cái nhìn tại Idris tutorial phần 7 Lần đọc và "với" quy tắc.