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