Czy można używać osłon w definicji funkcji w idris?

Question

w Haskell, można napisać:

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

Czy można napisać coś równoważnego w Idris, nie robiąc go ifThenElse (moje prawdziwe przypadku jest bardziej skomplikowany niż ten powyżej)?

Answer 1

Idris nie ma osłony wzoru dokładnie tak, jak w haskell. Jest z klauzuli, która jest składniowo podobny (ale bardziej wydajne, ponieważ obsługuje dopasowanie w obecności typów zależnych):

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

Można przyjrzeć się Idris tutorial sekcji 7 widoki i „z” zasadą.