The stream split at every LF: n LFs give n + 1 segments, the last the
bytes after the final LF (empty for a stream that ends with one).
115def aosSegments =
116 (lambda unrestricted stream : Bytes .
117 (bytes-eliminate
118 (lambda unrestricted current : Bytes . (family StdList Bytes))
119 (aosBytesCons b"" (constructor StdList StdListEmpty Bytes))
120 (lambda unrestricted head : Byte .
121 (lambda unrestricted tail : Bytes .
122 (lambda unrestricted induction : (family StdList Bytes) .
123 (nat-eliminate
124 (lambda unrestricted current : Nat . (family StdList Bytes))
125 (aosBytesCons (bytes-cons head (aosListHead induction)) (aosListTail induction))
126 (lambda unrestricted predecessor : Nat .
127 (lambda unrestricted inner : (family StdList Bytes) . (aosBytesCons b"" induction)))
128 (byte-equal head (byte 10))))))
129 stream))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.