syntax - idris の関数定義でガードを使用することは可能ですか?

Question

Haskell では、次のように記述できます。

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

Idris でそれを行わずに同等のものを書くことは可能ですかifThenElse(私の実際のケースは上記のものよりも複雑です)?

Answer 1

Idris には、haskell とまったく同じパターン ガードがありません。構文的に似ているwith句があります (ただし、依存型が存在する場合のマッチングをサポートするため、より強力です)。

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

Idris のチュートリアルセクション7 ビューと "with" ルールを参照してください。