|
|
|
|
|
|
by pyrale
3296 days ago
|
|
|
head [] in haskell will crash and burn, because you cannot carry vector size information in the type (at least not easily). In idris, you can lift the non-empty list check at type level, making such operation a compilation error. |
|
|