collectfilterfun2() ==
  tr.let n,b,c = tr in 
      case c
      of inl(x) => if snd(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 ,  pi2: snd(t),  inl: inl x ,  subtract: n - m,  natural_number: $n,  inr: inr x ,  it:
FDL editor aliases :  collectfilterfun2

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


Date html generated: 2010_08_27-PM-02_54_28
Last ObjectModification: 2010_03_26-PM-01_42_31

Home Index