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
Definitions occuring in Statement :
null: null(as),
list_ind: list_ind,
ifthenelse: if b then t else f fi ,
unit: Unit,
union: left + right
FDL editor aliases :
disjoint-union-type
Latex:
disjoint-union-type(L) == rec-case(L) of [] => Unit | T::Ts => r.if null(Ts) then T else T + r fi
Date html generated:
2016_05_17-AM-09_26_36
Last ObjectModification:
2012_11_29-AM-11_15_08
Theory : classrel!lemmas
Home
Index