Partial list
= Partial list
{title2=$x_1:\cdots:x_n:\bot$}
A <list> whose spine or elements may contain <bottom values>. The displayed value has a known finite spine prefix and an undefined tail. An entirely undefined list exposes no outer constructor, while `[]` exposes a terminating empty list. These distinctions matter to <strict functions> and to the <fold factorisation criterion>.