= Proper lazy list
A <proper lazy list> has a spine exposing either finitely many cons constructors followed by `[]`, or infinitely many cons constructors, without an undefined tail at a finite position. This is a condition on the spine: an element may itself be the <bottom value> without hiding the <list>'s constructors. A <partial list> with a finite visible prefix followed by $\bot$ fails this condition. The distinction supports <productivity> proofs that inspect constructors without evaluating the stored elements.
Back to article page
