Nuprl Definition : aa_list_filter_indices
aa_list_filter_indices(l) ==
rec-case(l) of
[] => 
f.[]
aa_head::aa_tail =>
rec.f.if f[0] then [aa_head / rec[n.f[n + 1]]] else rec[n.f[n + 1]] fi
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
so_apply: x[s],
lambda: x.A[x],
add: n + m,
natural_number: $n
FDL editor aliases :
aa_list_filter_indices
aa\_list\_filter\_indices(l) ==
rec-case(l) of
[] => \mlambda{}f.[]
aa$_{head}$::aa$_{tail}$ =>
rec.\mlambda{}f.if f[0] then [aa$_{head}$ / rec[\mlambda{}n.f[n + 1]]] else rec[\mlambda{}n.f[n + 1]] fi\000C
Date html generated:
2013_03_20-AM-09_51_46
Last ObjectModification:
2012_11_27-AM-10_32_11
Home
Index