Nuprl Definition : map-index_aux
map-index_aux(f;L) == rec-case(L) of [] => λn.[] | hd::tl => aux.λn.[f n hd / (aux (n + 1))]
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
apply: f a,
lambda: λx.A[x],
add: n + m,
natural_number: $n
Definitions occuring in definition :
list_ind: list_ind,
nil: [],
lambda: λx.A[x],
cons: [a / b],
apply: f a,
add: n + m,
natural_number: $n
FDL editor aliases :
map-index_aux
Latex:
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:
2016_05_14-PM-03_11_57
Last ObjectModification:
2015_09_22-PM-05_58_36
Theory : list_1
Home
Index