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