Nuprl Definition : qexpfact

qexpfact(n;x;p;b) ==
  fix((λqexpfact,n,p,b. if q_less(p;b)
                       then n
                       else eval n' = n + 1 in
                            eval p' = x * p in
                            eval b' = n' * b in
                              qexpfact n' p' b'
                       fi )) 
  n 
  p 
  b


Definitions occuring in Statement :  q_less: q_less(r;s),  qmul: r * s,  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  multiply: n * m,  add: n + m,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  q_less: q_less(r;s),  add: n + m,  natural_number: $n,  qmul: r * s,  callbyvalue: callbyvalue,  multiply: n * m,  apply: f a
FDL editor aliases :  qexpfact
Latex:
qexpfact(n;x;p;b)  ==
    fix((\mlambda{}qexpfact,n,p,b.  if  q\_less(p;b)
                                              then  n
                                              else  eval  n'  =  n  +  1  in
                                                        eval  p'  =  x  *  p  in
                                                        eval  b'  =  n'  *  b  in
                                                            qexpfact  n'  p'  b'
                                              fi  )) 
    n 
    p 
    b


Date html generated: 2016_05_15-PM-11_13_37
Last ObjectModification: 2015_09_23-AM-08_27_58

Theory : rationals


Home Index