Nuprl Definition : enum-fin-seq
enum-fin-seq(m) ==
primrec(m;[λx.tt];λi,r. (map(λs,x. if x=i then tt else (s x);r) @ map(λs,x. if x=i then ff else (s x);r)))
Definitions occuring in Statement :
map: map(f;as),
append: as @ bs,
cons: [a / b],
nil: [],
primrec: primrec(n;b;c),
bfalse: ff,
btrue: tt,
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
primrec: primrec(n;b;c),
cons: [a / b],
nil: [],
append: as @ bs,
btrue: tt,
map: map(f;as),
lambda: λx.A[x],
int_eq: if a=b then c else d,
bfalse: ff,
apply: f a
FDL editor aliases :
enum-fin-seq
Latex:
enum-fin-seq(m) ==
primrec(m;[\mlambda{}x.tt];\mlambda{}i,r. (map(\mlambda{}s,x. if x=i then tt else (s x);r)
@ map(\mlambda{}s,x. if x=i then ff else (s x);r)))
Date html generated:
2016_05_14-PM-09_46_30
Last ObjectModification:
2015_10_21-PM-05_58_12
Theory : continuity
Home
Index