Nuprl Definition : reduce2
reduce2(f;k;i;as) == fix((λreduce2,i,as. case as of [] => k | a::as' => f a i (reduce2 (i + 1) as') esac)) i as
Definitions occuring in Statement :
list_ind: list_ind,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
list_ind: list_ind,
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
reduce2
Latex:
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