Nuprl Definition : for_hdtl
ForHdTl{A,f,k} h::t ∈ as. g[h; t] == reduce(f;k;mapcons(λh,t. g[h; t];as))
Definitions occuring in Statement :
mapcons: mapcons(f;as),
reduce: reduce(f;k;as),
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
mapcons: mapcons(f;as),
lambda: λx.A[x]
FDL editor aliases :
for_hdtl
Latex:
ForHdTl\{A,f,k\} h::t \mmember{} as. g[h; t] == reduce(f;k;mapcons(\mlambda{}h,t. g[h; t];as))
Date html generated:
2016_05_14-AM-07_38_30
Last ObjectModification:
2015_12_21-PM-01_46_11
Theory : list_1
Home
Index