Nuprl Definition : real_term_value

real_term_value(f;t) ==
  int_term_ind(t;
               itermConstant(n) r(n);
               itermVar(v) v;
               itermAdd(l,r) rl,rr.rl rr;
               itermSubtract(l,r) rl,rr.rl rr;
               itermMultiply(l,r) rl,rr.rl rr;
               itermMinus(x) r.-(r)) 



Definitions occuring in Statement :  rsub: y rmul: b rminus: -(x) radd: b int-to-real: r(n) int_term_ind: int_term_ind apply: a
Definitions occuring in definition :  int_term_ind: int_term_ind int-to-real: r(n) apply: a radd: b rsub: y rmul: b rminus: -(x)
FDL editor aliases :  real_term_value

Latex:
real\_term\_value(f;t)  ==
    int\_term\_ind(t;
                              itermConstant(n){}\mRightarrow{}  r(n);
                              itermVar(v){}\mRightarrow{}  f  v;
                              itermAdd(l,r){}\mRightarrow{}  rl,rr.rl  +  rr;
                              itermSubtract(l,r){}\mRightarrow{}  rl,rr.rl  -  rr;
                              itermMultiply(l,r){}\mRightarrow{}  rl,rr.rl  *  rr;
                              itermMinus(x){}\mRightarrow{}  r.-(r)) 



Date html generated: 2017_10_02-PM-07_17_44
Last ObjectModification: 2017_04_02-PM-00_34_33

Theory : reals


Home Index