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