Ist es möglich, Wächter in der Funktionsdefinition in Idris zu verwenden?

Question

in Haskell, könnte man schreiben:

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

Ist es möglich, etwas Gleichwertiges in Idris zu schreiben, ohne es mit ifThenElse zu tun (meinem wirklichen Fall komplexer als die ist oben)?

Answer 1

Idris hat keine Musterwächter wie in Haskell. Es gibt mit Klausel, die syntaktisch ähnlich ist (aber leistungsstärker als es Anpassung in Anwesenheit von abhängigen Typen unterstützt):

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

Sie einen Blick darauf werfen kann an den Idris tutorial Abschnitt 7 Ansichten und den „mit“ -Regel.