Nuprl Definition : mapc
Illustration of use of add_rec_def for a curried function⋅
mapc(f) == fix((λmapc,f,as. case as of [] => [] | a::as1 => [f a / (mapc f as1)] esac)) f
Definitions occuring in Statement :
list_ind: list_ind,
cons: [a / b],
nil: [],
apply: f a,
fix: fix(F),
lambda: λx.A[x]
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
list_ind: list_ind,
nil: [],
cons: [a / b],
apply: f a
FDL editor aliases :
mapc
Latex:
mapc(f) == fix((\mlambda{}mapc,f,as. case as of [] => [] | a::as1 => [f a / (mapc f as1)] esac)) f
Date html generated:
2016_07_08-PM-04_48_00
Last ObjectModification:
2015_12_09-PM-01_58_45
Theory : list_0
Home
Index