Is it possible to use guards in function definition in idris?

Question

In haskell, one could write :

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

Is it possible to write something equivalent in Idris, without doing it with ifThenElse (my real case is more complex than the one above)?

Answer 1

Idris does not have pattern guards exactly as in haskell. There is with clause which is syntactically similar (but more powerful as it supports matching in presence of dependent types):

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

You can take a look at the Idris tutorial section 7 Views and the "with" rule.