Странное поведение сопоставления с образцом в Идрисе
Я наткнулся на то, что кажется странным для Идриса.
Я использую Emacs 25.3 на Ubuntu 17.04 и Idris 1.0.
Рассмотрим следующий модуль:
module Strange
%default total
fun : Int -> Int -> Int
fun 0 0 = 0
fun 0 n = 10
fun n 0 = 20
Когда я загружаю это (C-c C-l), Я не получаю предупреждение о неполной функции, и когда я пробую его на REPL, я получаю это:
λΠ> fun 100 200
20 : Int
... как будто Идрис не соответствует буквальному 0 в третьем пункте. Это происходит также при загрузке модуля в обычную оболочку (idris Strange.idr).
Разве я не должен получить какую-то ошибку о не совокупности? Это какая-то ошибка в этой версии Idris?