Nuprl Definition : tuple-type
tuple-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
, 
product: x:A × B[x]
Definitions occuring in definition : 
list_ind: list_ind, 
unit: Unit
, 
ifthenelse: if b then t else f fi 
, 
null: null(as)
, 
product: x:A × B[x]
FDL editor aliases : 
tuple-type
Latex:
tuple-type(L)  ==    rec-case(L)  of  []  =>  Unit  |  T::Ts  =>  r.if  null(Ts)  then  T  else  T  \mtimes{}  r  fi 
Date html generated:
2016_05_14-PM-03_57_19
Last ObjectModification:
2015_09_22-PM-06_01_58
Theory : tuples
Home
Index