Nuprl Definition : rat2real
rat2real(q) ==  if isint(q) then r(q) else let a,b = q in (r(a))/b fi 
Definitions occuring in Statement : 
int-rdiv: (a)/k1
, 
int-to-real: r(n)
, 
ifthenelse: if b then t else f fi 
, 
bfalse: ff
, 
btrue: tt
, 
isint: isint def, 
spread: spread def
Definitions occuring in definition : 
int-to-real: r(n)
, 
int-rdiv: (a)/k1
, 
spread: spread def, 
bfalse: ff
, 
btrue: tt
, 
isint: isint def, 
ifthenelse: if b then t else f fi 
FDL editor aliases : 
rat2real
Latex:
rat2real(q)  ==    if  isint(q)  then  r(q)  else  let  a,b  =  q  in  (r(a))/b  fi 
Date html generated:
2019_10_29-AM-09_58_59
Last ObjectModification:
2019_10_17-AM-11_31_29
Theory : reals
Home
Index