---

collectfilterfun() ==
  tr.let n,b,c = tr in 
      case c of inl(x) => if x then inl (n - 1)  else inr   fi  | inr(x) => c

---

Definitions :  lambda: x.A[x],  spreadn: spread3,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  ifthenelse: if b then t else f fi ,  inl: inl x ,  subtract: n - m,  natural_number: $n,  inr: inr x ,  it:
FDL editor aliases :  collectfilterfun

---

collectfilterfun()  ==
    \mlambda{}tr.let  n,b,c  =  tr  in 
            case  c  of  inl(x)  =>  if  x  then  inl  (n  -  1)    else  inr  \mcdot{}    fi    |  inr(x)  =>  c


Date html generated: 2010_08_27-PM-02_54_15
Last ObjectModification: 2010_03_26-PM-01_27_07

Home Index