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