---

ste-type(ste) ==
  st_exp_ind(ste)
  var(v)=>rho.(rho v)
  const(b)=>rho.(fst(b))
  f(a)=>rf,ra.rho.st-ap(rf rho;ra rho)
  x:st.b=>rb.rho.st_arrow(st;rb (z.if z =a x then st else rho z fi ))

---

Definitions occuring in Statement :  st_exp_ind: st_exp_ind,  st-ap: st-ap(st1;st2),  st_arrow: st_arrow(domain;range),  eq_atom: x =a y,  ifthenelse: if b then t else f fi ,  pi1: fst(t),  apply: f a,  lambda: x.A[x]
Definitions :  st_exp_ind: st_exp_ind,  pi1: fst(t),  st_arrow: Error :st_arrow,  lambda: x.A[x],  ifthenelse: if b then t else f fi ,  eq_atom: x =a y,  apply: f a
FDL editor aliases :  ste-type

---

ste-type(ste)  ==
    st\_exp\_ind(ste)
    var(v)=>\mlambda{}rho.(rho  v)
    const(b)=>\mlambda{}rho.(fst(b))
    f(a)=>rf,ra.\mlambda{}rho.st-ap(rf  rho;ra  rho)
    \mlambda{}x:st.b=>rb.\mlambda{}rho.st\_arrow(st;rb  (\mlambda{}z.if  z  =a  x  then  st  else  rho  z  fi  ))


Date html generated: 2011_08_17-PM-05_09_20
Last ObjectModification: 2011_02_04-PM-03_32_43

Home Index