Nuprl Definition : tuple

tuple(n;i.F[i]) ==  rec-case(map(λi.F[i];upto(n))) of [] => ⋅ a::as => r.if null(as) then else <a, r> fi 

Definitions occuring in Statement :  upto: upto(n) null: null(as) map: map(f;as) list_ind: list_ind ifthenelse: if then else fi  it: lambda: λx.A[x] pair: <a, b>
Definitions occuring in definition :  list_ind: list_ind map: map(f;as) lambda: λx.A[x] upto: upto(n) it: ifthenelse: if then else fi  null: null(as) pair: <a, b>
FDL editor aliases :  tuple

tuple(n;i.F[i])  ==
    rec-case(map(\mlambda{}i.F[i];upto(n)))  of
    []  =>  \mcdot{}
    a::as  =>
      r.if  null(as)  then  a  else  <a,  r>  fi 

Date html generated: 2016_05_14-PM-03_57_35
Last ObjectModification: 2015_09_22-PM-06_01_58

Theory : tuples

Home Index