syntaxpattern-matchingidrisguard-clause

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


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)?


Solution

  • 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.