Fold from the right: `stdListFold f z [a, b] = f a (f b z)`.
152def stdListFold =
153 (lambda erased element : Type 0 .
154 (lambda erased accumulator : Type 0 .
155 (lambda unrestricted step : (pi unrestricted value : element . (pi unrestricted carried : accumulator . accumulator)) .
156 (lambda unrestricted initial : accumulator .
157 (lambda unrestricted values : (family StdList element) .
158 (eliminate
159 StdList
160 (lambda unrestricted current : (family StdList element) . accumulator)
161 values
162 (branch StdListEmpty . initial)
163 (branch StdListCons head tail induction . (step head induction))))))))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.