Nuprl Definition : b-union
The union of two types is a special case of the union of a family of types,
where we use the booleans to index the family.⋅
A ⋃ B == ⋃x:𝔹.if x then A else B fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
bool: 𝔹,
tunion: ⋃x:A.B[x]
Definitions occuring in definition :
tunion: ⋃x:A.B[x],
bool: 𝔹,
ifthenelse: if b then t else f fi
Rules referencing :
StrongContinuity2
FDL editor aliases :
b-union
Latex:
A \mcup{} B == \mcup{}x:\mBbbB{}.if x then A else B fi
Date html generated:
2016_07_08-PM-04_46_48
Last ObjectModification:
2015_09_22-PM-05_44_33
Theory : union
Home
Index