Nuprl Definition : SM2-class-du
SM2-class-du(init;trX1;trX2) == let tr1,X1 = trX1 in let tr2,X2 = trX2 in Accum-loc-class(tr1 + tr2;init;X1 + X2)
Proof not projected
Definitions occuring in Statement :
disjoint-union-tr: tr1 + tr2,
disjoint-union-class: X + Y,
Accum-loc-class: Accum-loc-class(f;init;X),
spread: spread def
FDL editor aliases :
SM2-class-du
SM2-class-du(init;trX1;trX2) ==
let tr1,X1 = trX1
in let tr2,X2 = trX2
in Accum-loc-class(tr1 + tr2;init;X1 + X2)
Date html generated:
2011_10_20-PM-03_40_54
Last ObjectModification:
2011_09_23-PM-08_53_08
Home
Index