Можно ли использовать защиту в определении функции в idris?

В haskell можно написать:

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

Можно ли написать что-то эквивалентное в Идрисе, не делая этого с помощью ifThenElse (мой реальный случай более сложный, чем тот, который был выше)?

Ответы

Ответ 1

Идрис не имеет шаблонов, точно так же, как в haskell. Существует предложение с, которое синтаксически похоже (но более мощное, поскольку оно поддерживает сопоставление в присутствии зависимых типов):

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

Вы можете посмотреть Idris tutorial раздел 7 просмотров и правило "с" .