Nuprl Definition : alpha-rename-alist

alpha-rename-alist(t;L) ==
  snd(accumulate (with value p and list item x):
       let vs,tab = p 
       in eval x' = maybe_new_var(x;vs) in
          <[x' / vs], [<x, x'> / tab]>
      over list:
        L
      with starting value:
       <L @ all-vars(t), []>))


Definitions occuring in Statement :  all-vars: all-vars(t),  maybe_new_var: maybe_new_var(v;vs),  append: as @ bs,  list_accum: list_accum,  cons: [a / b],  nil: [],  callbyvalue: callbyvalue,  pi2: snd(t),  spread: spread def,  pair: <a, b>
Definitions occuring in definition :  pi2: snd(t),  list_accum: list_accum,  spread: spread def,  callbyvalue: callbyvalue,  maybe_new_var: maybe_new_var(v;vs),  cons: [a / b],  pair: <a, b>,  append: as @ bs,  all-vars: all-vars(t),  nil: []
FDL editor aliases :  alpha-rename-alist
Latex:
alpha-rename-alist(t;L)  ==
    snd(accumulate  (with  value  p  and  list  item  x):
              let  vs,tab  =  p 
              in  eval  x'  =  maybe\_new\_var(x;vs)  in
                    <[x'  /  vs],  [<x,  x'>  /  tab]>
            over  list:
                L
            with  starting  value:
              <L  @  all-vars(t),  []>))


Date html generated: 2020_05_19-PM-09_57_07
Last ObjectModification: 2020_03_09-PM-04_09_33

Theory : terms


Home Index