= Direct fold obstruction for dropping a prefix
Suppose a <predicate> accepts some $u$ and rejects some $v$. Dropping its initial accepted <list prefix> maps both the empty <list> and the singleton $u$ to the empty <list>, but maps the extensions by $v$ to different <lists>. A direct <list fold> cannot do this: its combining <function> receives the same head and the same folded-tail summary in both cases. This is an instance of the <fold factorisation criterion>. An auxiliary <list fold> retaining more information followed by projection is not ruled out.
Back to article page
