Nuprl Definition : list_accum'
list_accum'(f;v;L)==r if null(L) then v else let v' ⟵ f v L in let a,as = L in list_accum'(f;v';as) fi
list_accum'(f;v;L) ==
fix((λlist_accum',v,L. if null(L) then v else let v' ⟵ f v L in let a,as = L in list_accum' v' as fi )) v L
Definitions occuring in Statement :
null: null(as),
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
apply: f a,
spread: spread def,
callbyvalueall: callbyvalueall,
null: null(as),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
fix: fix(F)
FDL editor aliases :
list_accum'
list_accum'
Latex:
list\_accum'(f;v;L)
==r if null(L) then v else let v' \mleftarrow{}{} f v L in let a,as = L in list\_accum'(f;v';as) fi
Latex:
list\_accum'(f;v;L) ==
fix((\mlambda{}list$_{accum'}$,v,L. if null(L)
then v
else let v' \mleftarrow{}{} f v L
in let a,as = L
in list$_{accum'}$ v' as
fi ))
v
L
Date html generated:
2017_04_14-AM-08_48_22
Last ObjectModification:
2017_04_10-PM-10_32_41
Theory : list_0
Home
Index