Idris (programming language): Difference between revisions

Revision as of 20:55, 11 April 2021

Revision as of 16:58, 19 June 2021

Line 87:

</syntaxhighlight>

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. SinceBecause boththe vectorstype aresystem ensuredcan byprove that the type system tovectors have exactly the same length, we can be sure at compile time that this case will not occur. Henceand itthere doesis notno need to beinclude mentionedthat forcase in the function to befunction’s totaldefinition.

===Proof assistant features===