I stumbled upon what seems to be a strange behavior for Idris.
I'm using Emacs 25.3 on Ubuntu 17.04 and Idris 1.0.
Consider the following module:
module Strange
%default total
fun : Int -> Int -> Int
fun 0 0 = 0
fun 0 n = 10
fun n 0 = 20
When I load this (C-c C-l), I do not get a non-total function warning, and when I try it on the REPL I get this:
λΠ> fun 100 200
20 : Int
... as if Idris is not matching the literal 0 in the third clause. This behavior occurs also when loading the module in a normal shell (idris Strange.idr).
Shouldn't I get some kind of error about non-totality? Is this some bug in this version of Idris?