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