Nuprl Definition : replace-vars

replace-vars(s;t) ==
  case t
   of inl(v) =>
   case apply-alist(VarDeq;s;v) of inl(a) => a | inr(_) => t
   | inr(p) =>
   let op,bts = p 
   in eval bts' = eager-map(λbt.let vs,b = bt 
                                in <vs, replace-vars(s;b)>;bts) in
      mkterm(op;bts')


Definitions occuring in Statement :  mkterm: mkterm(opr;bts),  var-deq: VarDeq,  apply-alist: apply-alist(eq;L;x),  eager-map: eager-map(f;as),  callbyvalue: callbyvalue,  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],  apply-alist: apply-alist(eq;L;x),  var-deq: VarDeq,  callbyvalue: callbyvalue,  eager-map: eager-map(f;as),  lambda: λx.A[x],  spread: spread def,  pair: <a, b>,  mkterm: mkterm(opr;bts)
FDL editor aliases :  replace-vars
Latex:
replace-vars(s;t)  ==
    case  t
      of  inl(v)  =>
      case  apply-alist(VarDeq;s;v)  of  inl(a)  =>  a  |  inr($_{}$)  =>  t
      |  inr(p)  =>
      let  op,bts  =  p 
      in  eval  bts'  =  eager-map(\mlambda{}bt.let  vs,b  =  bt 
                                                                in  <vs,  replace-vars(s;b)>bts)  in
            mkterm(op;bts')


Date html generated: 2020_05_19-PM-09_57_29
Last ObjectModification: 2020_03_09-PM-04_09_46

Theory : terms


Home Index