Nuprl Definition : callbyvalueall_seq
callbyvalueall_seq(L;G;F;n;m) ==
fix((λcallbyvalueall_seq,G,n. if m ≤z n then F G else let v ⟵ G (L n) in callbyvalueall_seq (λf.(G f v)) (n + 1) fi )\000C) G n
Definitions occuring in Statement :
le_int: i ≤z j,
callbyvalueall: callbyvalueall,
ifthenelse: if b then t else f fi ,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
ifthenelse: if b then t else f fi ,
le_int: i ≤z j,
callbyvalueall: callbyvalueall,
lambda: λx.A[x],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
callbyvalueall_seq
Latex:
callbyvalueall\_seq(L;G;F;n;m) ==
fix((\mlambda{}callbyvalueall$_{seq}$,G,n. if m \mleq{}z n
then F G
else let v \mleftarrow{}{} G (L n)
in callbyvalueall$_{seq}$ (\mlambda{}f.(G f v)) (n + 1\000C)
fi ))
G
n
Date html generated:
2016_05_15-PM-02_09_24
Last ObjectModification:
2015_09_23-AM-07_38_04
Theory : untyped!computation
Home
Index