Nuprl Definition : combinations_aux

combinations_aux(b;n;m) ==
  fix((λcombinations_aux,b,n,m. if (n =z 0)
                               then b
                               else eval b2 = b * m in
                                    eval n2 = n - 1 in
                                    eval m2 = m - 1 in
                                      combinations_aux b2 n2 m2
                               fi )) 
  b 
  n 
  m


Definitions occuring in Statement :  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  multiply: n * m,  callbyvalue: callbyvalue,  subtract: n - m,  natural_number: $n,  apply: f a
FDL editor aliases :  combinations_aux
Latex:
combinations\_aux(b;n;m)  ==
    fix((\mlambda{}combinations$_{aux}$,b,n,m.  if  (n  =\msubz{}  0)
                                                            then  b
                                                            else  eval  b2  =  b  *  m  in
                                                                      eval  n2  =  n  -  1  in
                                                                      eval  m2  =  m  -  1  in
                                                                          combinations$_{aux}$  b2  n2  m2
                                                            fi  )) 
    b 
    n 
    m


Date html generated: 2016_05_15-PM-05_57_19
Last ObjectModification: 2015_09_23-AM-08_00_19

Theory : general


Home Index