Comment by notjack

You probably could, but part of the purpose of Idris is to statically prove things with dependent types rather than test them.