Nuprl Definition : rP_to_term

rP_to_term(stack;L)
==r if L = Ax then stack otherwise let op,more = L 
                                   in if op=1
                                         then let c,evenmore = more 
                                              in rP_to_term(["c" / stack];evenmore)
                                         else if op=2
                                                 then let v,evenmore = more 
                                                      in rP_to_term([vv / stack];evenmore)
                                                 else if op=3
                                                         then let q,p,s = stack in 
                                                              rP_to_term([p (+) q / s];more)
                                                         else if op=4
                                                                 then let q,p,s = stack in 
                                                                      rP_to_term([p (-) q / s];more)
                                                                 else if op=5
                                                                         then let q,p,s = stack in 
                                                                              rP_to_term([p (*) q / s];more)
                                                                         else let p,s = stack 
                                                                              in rP_to_term(["-"p / s];more)
rP_to_term(stack;L) ==
  fix((λrP_to_term,stack,L. if L = Ax then stack
                            otherwise let op,more = L 
                                      in if op=1
                                            then let c,evenmore = more 
                                                 in rP_to_term ["c" / stack] evenmore
                                            else if op=2
                                                    then let v,evenmore = more 
                                                         in rP_to_term [vv / stack] evenmore
                                                    else if op=3
                                                            then let q,p,s = stack in 
                                                                 rP_to_term [p (+) q / s] more
                                                            else if op=4
                                                                    then let q,p,s = stack in 
                                                                         rP_to_term [p (-) q / s] more
                                                                    else if op=5
                                                                            then let q,p,s = stack in 
                                                                                 rP_to_term [p (*) q / s] more
                                                                            else let p,s = stack 
                                                                                 in rP_to_term ["-"p / s] more)) 
  stack 
  L


Definitions occuring in Statement :  itermMinus: "-"num,  itermMultiply: left (*) right,  itermSubtract: left (-) right,  itermAdd: left (+) right,  itermVar: vvar,  itermConstant: "const",  cons: [a / b],  spreadn: spread3,  isaxiom: if z = Ax then a otherwise b,  int_eq: if a=b  then c  else d,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def,  natural_number: $n
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  isaxiom: if z = Ax then a otherwise b,  itermConstant: "const",  itermVar: vvar,  itermAdd: left (+) right,  itermSubtract: left (-) right,  int_eq: if a=b  then c  else d,  natural_number: $n,  spreadn: spread3,  itermMultiply: left (*) right,  spread: spread def,  apply: f a,  cons: [a / b],  itermMinus: "-"num
FDL editor aliases :  rP_to_term
Latex:
rP\_to\_term(stack;L)
==r  if  L  =  Ax  then  stack
        otherwise  let  op,more  =  L 
                            in  if  op=1
                                        then  let  c,evenmore  =  more 
                                                  in  rP\_to\_term(["c"  /  stack];evenmore)
                                        else  if  op=2
                                                        then  let  v,evenmore  =  more 
                                                                  in  rP\_to\_term([vv  /  stack];evenmore)
                                                        else  if  op=3
                                                                        then  let  q,p,s  =  stack  in 
                                                                                  rP\_to\_term([p  (+)  q  /  s];more)
                                                                        else  if  op=4
                                                                                        then  let  q,p,s  =  stack  in 
                                                                                                  rP\_to\_term([p  (-)  q  /  s];more)
                                                                                        else  if  op=5
                                                                                                        then  let  q,p,s  =  stack  in 
                                                                                                                  rP\_to\_term([p  (*)  q  /  s];more)
                                                                                                        else  let  p,s  =  stack 
                                                                                                                  in  rP\_to\_term(["-"p  /  s];more)
Latex:
rP\_to\_term(stack;L)  ==
    fix((\mlambda{}rP\_to$_{term}$,stack,L.
                                                    if  L  =  Ax  then  stack
                                                    otherwise  let  op,more  =  L 
                                                                        in  if  op=1
                                                                                    then  let  c,evenmore  =  more 
                                                                                              in  rP\_to$_{term}$  ["c"  /  stack]  e\000Cvenmore
                                                                                    else  if  op=2
                                                                                                    then  let  v,evenmore  =  more 
                                                                                                              in  rP\_to$_{term}$  [vv  /  s\000Ctack]  evenmore
                                                                                                    else  if  op=3
                                                                                                                    then  let  q,p,s  =  stack  in 
                                                                                                                              rP\_to$_{term}$  [p\000C  (+)  q  /  s]  more
                                                                                                                    else  if  op=4
                                                                                                                                    then  let  q,p,s  =  stack  in 
                                                                                                                                              rP\_to$_{term}\000C$  [p  (-)  q  /  s]  more
                                                                                                                                    else  if  op=5
                                                                                                                                                    then  let  q,p,s  =  stack  in 
                                                                                                                                                              rP\_to$_{t\000Cerm}$ 
                                                                                                                                                              [p  (*)  q  /  s] 
                                                                                                                                                              more
                                                                                                                                                    else  let  p,s  =  stack 
                                                                                                                                                              in  rP\_to$_\mbackslash{}ff\000C7bterm}$ 
                                                                                                                                                                    ["-"p  /  s] 
                                                                                                                                                                    more)) 
    stack 
    L


Date html generated: 2017_09_29-PM-05_55_01
Last ObjectModification: 2017_05_12-PM-08_33_35

Theory : omega


Home Index