Fold from the head: `step (... (step (step initial x0) x1) ...) xn`.
stdListFold visits the LAST element first (its step sees the folded tail);
this visits the FIRST element first and threads the accumulator forward,
which is the order a floating-point accumulation or a reverse-time pass over
a newest-first history must respect (the results differ when the step does
not associate, e.g. f32 addition). The list is eliminated into a function of
the accumulator, so the recursion is still structural.
172def stdListFoldFromHead =
173 (lambda erased element : Type 0 .
174 (lambda erased accumulator : Type 0 .
175 (lambda unrestricted step : (pi unrestricted carried : accumulator . (pi unrestricted value : element . accumulator)) .
176 (lambda unrestricted initial : accumulator .
177 (lambda unrestricted values : (family StdList element) .
178 (app
179 (eliminate
180 StdList
181 (lambda unrestricted current : (family StdList element) . (pi unrestricted carried : accumulator . accumulator))
182 values
183 (branch StdListEmpty . (lambda unrestricted carried : accumulator . carried))
184 (branch StdListCons head tail induction .
185 (lambda unrestricted carried : accumulator . (induction (step carried head)))))
186 initial))))))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.