Nuprl Definition : reduce

Reduce is the foldr operation⋅
reduce(f;k;as) ==  rec-case(as) of [] => k | a::as' => r.f a r


Definitions occuring in Statement :  list_ind: list_ind,  apply: f a
Definitions occuring in definition :  list_ind: list_ind,  apply: f a
FDL editor aliases :  reduce
Latex:
reduce(f;k;as)  ==    rec-case(as)  of  []  =>  k  |  a::as'  =>  r.f  a  r


Date html generated: 2016_07_08-PM-04_47_58
Last ObjectModification: 2015_12_09-PM-02_05_48

Theory : list_0


Home Index