Nuprl Definition : disjoint-union-type
disjoint-union-type(L) == rec-case(L) of [] => Unit | T::Ts => r.if null(Ts) then T else T + r fi
Proof not projected
Definitions occuring in Statement :
null: null(as),
ifthenelse: if b then t else f fi ,
unit: Unit,
union: left + right,
list_ind: list_ind def
FDL editor aliases :
disjoint-union-type
disjoint-union-type(L) == rec-case(L) of [] => Unit | T::Ts => r.if null(Ts) then T else T + r fi
Date html generated:
2011_10_20-PM-03_39_22
Last ObjectModification:
2011_09_22-PM-08_23_28
Home
Index