Nuprl Definition : mklist
mklist(n;f) == primrec(n;[];λi,l. (l @ [f i]))
Definitions occuring in Statement :
append: as @ bs,
cons: [a / b],
nil: [],
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
append: as @ bs,
cons: [a / b],
apply: f a,
nil: []
FDL editor aliases :
mklist
Latex:
mklist(n;f) == primrec(n;[];\mlambda{}i,l. (l @ [f i]))
Date html generated:
2016_05_14-PM-01_44_16
Last ObjectModification:
2015_09_22-PM-05_54_40
Theory : list_1
Home
Index