Nuprl Definition : val-union
val-union(eq;as;bs) == let as ⟵ as in let bs ⟵ bs in reduce(λa,L. insert(a;L);as;bs)
Definitions occuring in Statement :
insert: insert(a;L),
reduce: reduce(f;k;as),
callbyvalueall: callbyvalueall,
lambda: λx.A[x]
Definitions occuring in definition :
callbyvalueall: callbyvalueall,
reduce: reduce(f;k;as),
lambda: λx.A[x],
insert: insert(a;L)
FDL editor aliases :
val-union
Latex:
val-union(eq;as;bs) == let as \mleftarrow{}{} as in let bs \mleftarrow{}{} bs in reduce(\mlambda{}a,L. insert(a;L);as;bs)
Date html generated:
2016_05_14-PM-03_25_17
Last ObjectModification:
2015_09_22-PM-05_59_41
Theory : decidable!equality
Home
Index