Est-il possible d'utiliser des gardes dans la définition de fonction dans idris?

Question

En haskell, on pourrait écrire:

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

Est-il possible d'écrire quelque chose d'équivalent à Idris, sans le faire avec ifThenElse (mon cas réel est plus complexe que celui ci-dessus)?

Answer 1

Idris n'a pas de protections de motif exactement comme dans le haskell. Il y a avec clause qui est syntaxiquement similaire (mais plus puissant car il prend en charge l'appariement en présence de types dépendants):

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

Vous pouvez jeter un oeil à la section Idris tutorial7 Vues et « par » règle.