3 ms·
Unless length of the list (a "Vector" in typical dependent type nomenclature) I can see the issue. I have not read the paper, but why is not a the empty list t
by ObscureScience 3y ago
Unless length of the list (a "Vector" in typical dependent type nomenclature) I can see the issue.
I have not read the paper, but why is not a the empty list the value that returns None when called with this function? I assume the empty list is still a list in this type system?
- jmgrosen 3y agoNo, it’s not—-they’re passing in a “node”, not a list, which always contains both a head element and a (nullable) tail pointer. That’s why it can’t separate the head in the case of size one: the node must maintain a non-null head.