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?
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?