Idris (programming language): Difference between revisions

Revision as of 23:13, 10 November 2014

Revision as of 20:33, 13 November 2014

Line 62:

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 are ensured by the type system to have exactly the same length, we can be sure at compile time that this case will not occur. Hence it does not need to be mentioned for the function to be total.

==Features==

(in progress)

==References==