Idris (programming language): Difference between revisions

Revision as of 19:56, 16 April 2013

Revision as of 16:35, 23 April 2013

Line 49:

</source>

The functions appends a vector of m elements of type a to a vector of n elements of type a. Since the precise types of the input vectors depend on a value, it is possible to be cartaincertain at compile-time that the resulting vector will be have exactly (n + m) elements of type a.

The word "total" invokes the [[Partial function|totality checker]] which will report an error if the marked function doesn't cover all possible cases.