Idris (programming language): Difference between revisions

Revision as of 22:04, 7 May 2014

Revision as of 17:14, 18 June 2014

Line 61:

</source>

Num a signifies that the type a belongs to the [[type class]] Num. Note that this function is still typechecks successfully as total, even though there is no case matching Nil in one vector and a number in the other. Since both vectors must have, ensured via type system, exactly the same length we can be sure at compile time that this is a case that will not occur. Hence it does not need to be mentioned for the function to be total.

==References==