Nuprl Definition : mapc

Illustration of use of add_rec_def for curried function⋅

mapc(f) ==  fix((λmapc,f,as. case as of [] => [] a::as1 => [f (mapc as1)] esac)) f

Definitions occuring in Statement :  list_ind: list_ind cons: [a b] nil: [] apply: 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: a
FDL editor aliases :  mapc

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