13

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

Will Ness
  • 70,110
  • 9
  • 98
  • 181
Molochdaa
  • 2,158
  • 1
  • 17
  • 23

1 Answers1

15

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.

max taldykin
  • 12,459
  • 5
  • 45
  • 64
  • 6
    That's not the same as guards in the example Haskell which would allow for stuff like `| x+y == 10 ... | func (x * y + 52) > 42 = ...`. – Noein Aug 19 '15 at 19:27