Nuprl Definition : alpha-rename-aux

alpha-rename-aux(f;bnds;t) ==
  case t
   of inl(v) =>
   if v ∈b bnds then varterm(f v) else t fi 
   | inr(p) =>
   let op,bts = p 
   in eval bts' = eager-map(λbt.let vs,a = bt 
                                in <map(f;vs), alpha-rename-aux(f;rev(vs) + bnds;a)>;bts) in
      mkterm(op;bts')


Definitions occuring in Statement :  mkterm: mkterm(opr;bts),  varterm: varterm(v),  var-deq: VarDeq,  deq-member: x ∈b L,  rev-append: rev(as) + bs,  eager-map: eager-map(f;as),  map: map(f;as),  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  deq-member: x ∈b L,  var-deq: VarDeq,  varterm: varterm(v),  apply: f a,  callbyvalue: callbyvalue,  eager-map: eager-map(f;as),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  map: map(f;as),  rev-append: rev(as) + bs,  mkterm: mkterm(opr;bts)
FDL editor aliases :  alpha-rename-aux
Latex:
alpha-rename-aux(f;bnds;t)  ==
    case  t
      of  inl(v)  =>
      if  v  \mmember{}\msubb{}  bnds  then  varterm(f  v)  else  t  fi 
      |  inr(p)  =>
      let  op,bts  =  p 
      in  eval  bts'  =  eager-map(\mlambda{}bt.let  vs,a  =  bt 
                                                                in  <map(f;vs),  alpha-rename-aux(f;rev(vs)  +  bnds;a)>bts)  in
            mkterm(op;bts')


Date html generated: 2020_05_19-PM-09_56_32
Last ObjectModification: 2020_03_09-PM-04_09_25

Theory : terms


Home Index