map-index_aux(f;L) ==
rec-case(L) of [] => 
n.[] | hd::tl => aux.n.[f n hd / (aux (n + 1))]
Definitions :
list_ind: rec-case(a) of [] => s | x::y => z.t[x; y; z],
nil: [],
lambda: x.A[x],
cons: [car / cdr],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
map-index_aux
map-index\_aux(f;L) == rec-case(L) of [] => \mlambda{}n.[] | hd::tl => aux.\mlambda{}n.[f n hd / (aux (n + 1))]
Date html generated:
2010_08_27-PM-08_46_03
Last ObjectModification:
2010_03_18-PM-02_02_49
Home
Index