Nuprl Definition : real_term_value

real_term_value(f;t) ==
  int_term_ind(t;
               itermConstant(n)⇒ r(n);
               itermVar(v)⇒ f 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: x - y,  rmul: a * b,  rminus: -(x),  radd: a + b,  int-to-real: r(n),  int_term_ind: int_term_ind,  apply: f a
Definitions occuring in definition :  int_term_ind: int_term_ind,  int-to-real: r(n),  apply: f a,  radd: a + b,  rsub: x - y,  rmul: a * 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