Nuprl Definition : rev-map-append

rev-map-append(f;as;bs)
==r eval aa = as in
    if aa is a pair then let a,more = aa 
                         in eval b = f a in
                            rev-map-append(f;more;[b / bs]) otherwise bs
rev-map-append(f;as;bs) ==
  fix((λrev-map-append,as,bs. eval aa = as in
                              if aa is a pair then let a,more = aa 
                                                   in eval b = f a in
                                                      rev-map-append more [b / bs] otherwise bs)) 
  as 
  bs


Definitions occuring in Statement :  cons: [a / b],  callbyvalue: callbyvalue,  ispair: if z is a pair then a otherwise b,  apply: f a,  fix: fix(F),  lambda: λx.A[x],  spread: spread def
Definitions occuring in definition :  fix: fix(F),  lambda: λx.A[x],  ispair: if z is a pair then a otherwise b,  spread: spread def,  callbyvalue: callbyvalue,  apply: f a,  cons: [a / b]
FDL editor aliases :  rev-map-append
Latex:
rev-map-append(f;as;bs)
==r  eval  aa  =  as  in
        if  aa  is  a  pair  then  let  a,more  =  aa 
                                                  in  eval  b  =  f  a  in
                                                        rev-map-append(f;more;[b  /  bs])  otherwise  bs
Latex:
rev-map-append(f;as;bs)  ==
    fix((\mlambda{}rev-map-append,as,bs.  eval  aa  =  as  in
                                                            if  aa  is  a  pair  then  let  a,more  =  aa 
                                                                                                      in  eval  b  =  f  a  in
                                                                                                            rev-map-append  more  [b  /  bs]  otherwise  bs)) 
    as 
    bs


Date html generated: 2017_09_29-PM-05_58_48
Last ObjectModification: 2017_04_26-PM-00_51_14

Theory : list_1


Home Index