Nuprl Definition : reduce2

reduce2(f;k;i;as) ==  fix((λreduce2,i,as. case as of [] => a::as' => (reduce2 (i 1) as') esac)) as

Definitions occuring in Statement :  list_ind: list_ind apply: a fix: fix(F) lambda: λx.A[x] add: m natural_number: $n
Definitions occuring in definition :  fix: fix(F) lambda: λx.A[x] list_ind: list_ind apply: a add: m natural_number: $n
FDL editor aliases :  reduce2

reduce2(f;k;i;as)  ==
    fix((\mlambda{}reduce2,i,as.  case  as  of  []  =>  k  |  a::as'  =>  f  a  i  (reduce2  (i  +  1)  as')  esac))  i  as

Date html generated: 2016_05_15-PM-01_56_28
Last ObjectModification: 2015_09_23-AM-07_37_30

Theory : list!

Home Index