Nuprl Definition : finite-nat-seq-to-list
finite-nat-seq-to-list(f) == let n,s = f in primrec(n;[];λi,r. (r @ [s i]))
Definitions occuring in Statement :
append: as @ bs,
cons: [a / b],
nil: [],
primrec: primrec(n;b;c),
apply: f a,
lambda: λx.A[x],
spread: spread def
Definitions occuring in definition :
spread: spread def,
primrec: primrec(n;b;c),
lambda: λx.A[x],
append: as @ bs,
cons: [a / b],
apply: f a,
nil: []
FDL editor aliases :
finite-nat-seq-to-list
Latex:
finite-nat-seq-to-list(f) == let n,s = f in primrec(n;[];\mlambda{}i,r. (r @ [s i]))
Date html generated:
2016_05_14-PM-09_54_45
Last ObjectModification:
2016_01_15-AM-09_31_50
Theory : continuity
Home
Index