Nuprl Definition : evalall
evalall(t) ==
fix((λevalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall outl(x) in
inl y
else if x is inr then eval y = evalall outr(x) in
inr y
else x))
t
Definitions occuring in Statement :
callbyvalue: callbyvalue,
outr: outr(x),
outl: outl(x),
ispair: if z is a pair then a otherwise b,
isinr: isinr def,
isinl: isinl def,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
spread: spread def,
pair: <a, b>,
inr: inr x ,
inl: inl x
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ispair: if z is a pair then a otherwise b,
spread: spread def,
pair: <a, b>,
isinl: isinl def,
outl: outl(x),
inl: inl x,
isinr: isinr def,
callbyvalue: callbyvalue,
apply: f a,
outr: outr(x),
inr: inr x
FDL editor aliases :
evalall
Latex:
evalall(t) ==
fix((\mlambda{}evalall,t. eval x = t in
if x is a pair then let a,b = x
in eval a' = evalall a in
eval b' = evalall b in
<a', b'> otherwise if x is inl then eval y = evalall
outl(x) in
inl y
else if x is inr
eval y = evalall outr(x) in
inr y
else x))
t
Date html generated:
2017_09_29-PM-05_47_00
Last ObjectModification:
2017_04_25-PM-04_17_29
Theory : call!by!value_1
Home
Index