Builtin length has a weird implementation

[Negabinary]

Maybe it's marginally faster in the [?] case but I think it's probably slower for every other list, and it's also kinda weird to work with in proofs.

[7h3kk1d]

Hear me out:

(fix length -> fun xs -> case xs
| [] => 0
| [x1] => 1
| [x1, x2] => 2
| [x1, x2, x3] => 3
| [x1, x2, x3, x4] => 4
| [x1, x2, x3, x4, x5] => 5
| [x1, x2, x3, x4, x5, x6] => 6
| [x1, x2, x3, x4, x5, x6, x7] => 7
| [x1, x2, x3, x4, x5, x6, x7, x8] => 8
| [x1, x2, x3, x4, x5, x6, x7, x8, x9] => 9
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10] => 10
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11] => 11
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12] => 12
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13] => 13
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14] => 14
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15] => 15
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16] => 16
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17] => 17
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18] => 18
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19] => 19
| [x1, x2, x3, x4, x5, x6, x7, x8, x9, x10, x11, x12, x13, x14, x15, x16, x17, x18, x19, x20] => 20
| _::xs => 1 + length(xs)
end)