Nuprl Definition : tree2fun

tree2fun(eq;w;g) ==
  let d,f = w 
  in case d of inl(n) => n | inr(m) => eval x = g m in tree2fun(eq;f x;λi.if eq i m then x else g i fi )


Definitions occuring in Statement :  callbyvalue: callbyvalue,  ifthenelse: if b then t else f fi ,  apply: f a,  lambda: λx.A[x],  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y]
Definitions occuring in definition :  spread: spread def,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  callbyvalue: callbyvalue,  lambda: λx.A[x],  ifthenelse: if b then t else f fi ,  apply: f a
FDL editor aliases :  tree2fun
Latex:
tree2fun(eq;w;g)  ==
    let  d,f  =  w 
    in  case  d
            of  inl(n)  =>
            n
            |  inr(m)  =>
            eval  x  =  g  m  in
            tree2fun(eq;f  x;\mlambda{}i.if  eq  i  m  then  x  else  g  i  fi  )


Date html generated: 2019_06_20-PM-03_08_23
Last ObjectModification: 2018_08_13-AM-11_52_44

Theory : continuity


Home Index