Nuprl Definition : projn
projn(n;x) == fix((λprojn,n,x. if (n =z 1) then fst(x) else projn (n - 1) (snd(x)) fi )) n x
Definitions occuring in Statement :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pi1: fst(t),
pi2: snd(t),
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
fix: fix(F),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pi1: fst(t),
apply: f a,
subtract: n - m,
natural_number: $n,
pi2: snd(t)
FDL editor aliases :
projn
Latex:
projn(n;x) == fix((\mlambda{}projn,n,x. if (n =\msubz{} 1) then fst(x) else projn (n - 1) (snd(x)) fi )) n x
Date html generated:
2016_05_15-PM-03_26_51
Last ObjectModification:
2015_09_23-AM-07_43_22
Theory : general
Home
Index