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

Question

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

В хаскеле можно написать:

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

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

13

syntax pattern-matching idris guard-clause

Источник

user1037243 27 июл '14 в 13:04

1 ответ

Решение

Другие вопросы по тегам syntax pattern-matching idris guard-clause

user147057 27 июл '14 в 14:10 2014-07-27 14:10 · Accepted Answer · 2014-07-27 14:10

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

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

Вы можете взглянуть на раздел 7 Представлений учебника Idris и правило "с".