Nuprl Definition : norm-union
norm-union(Na;Nb) == λu.case u of inl(a) => eval a' = Na a in inl a' | inr(b) => eval b' = Nb b in inr b'
Definitions occuring in Statement :
callbyvalue: callbyvalue,
apply: f a,
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inr: inr x ,
inl: inl x
Definitions occuring in definition :
lambda: λx.A[x],
decide: case b of inl(x) => s[x] | inr(y) => t[y],
inl: inl x,
callbyvalue: callbyvalue,
apply: f a,
inr: inr x
FDL editor aliases :
norm-union
Latex:
norm-union(Na;Nb) ==
\mlambda{}u.case u of inl(a) => eval a' = Na a in inl a' | inr(b) => eval b' = Nb b in inr b'
Date html generated:
2016_05_13-PM-03_46_17
Last ObjectModification:
2015_09_22-PM-05_45_14
Theory : call!by!value_2
Home
Index