È possibile utilizzare le protezioni nella definizione della funzione in idris?

Question

a Haskell, si potrebbe scrivere:

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

E 'possibile scrivere qualcosa di equivalente a Idris, senza farlo con ifThenElse (il mio caso reale è più complessa di quella di cui sopra)?

Answer 1

Idris non ha protezioni modello esattamente come in haskell. C'è con clausola che è sintatticamente simile (ma più potente in quanto supporta corrispondente in presenza di tipi dipendenti):

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

si può prendere uno sguardo ai Idris tutorial sezione 7 Visualizzazioni e il "con" regola.