Idris (programming language): Difference between revisions

Revision as of 20:24, 16 July 2014

Revision as of 14:57, 30 July 2014

Line 61:

</source>

Num a signifies that the type a belongs to the [[type class]] Num. Note that this function 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,are ensured viaby the type system, to have 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==