Nuprl Definition : polyconst
polyconst(n;k)==r if n=0 then k else if k=0 then [] else [polyconst(n - 1;k)]
polyconst(n;k) == fix((λpolyconst,n. if n=0 then k else if k=0 then [] else [polyconst (n - 1)])) n
Definitions occuring in Statement :
cons: [a / b],
nil: [],
int_eq: if a=b then c else d,
apply: f a,
fix: fix(F),
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
nil: [],
natural_number: $n,
subtract: n - m,
apply: f a,
cons: [a / b],
int_eq: if a=b then c else d,
lambda: λx.A[x],
fix: fix(F)
FDL editor aliases :
polyconst
polyconst
Latex:
polyconst(n;k)==r if n=0 then k else if k=0 then [] else [polyconst(n - 1;k)]
Latex:
polyconst(n;k) == fix((\mlambda{}polyconst,n. if n=0 then k else if k=0 then [] else [polyconst (n - 1)]\000C)) n
Date html generated:
2017_04_20-AM-07_10_18
Last ObjectModification:
2017_04_17-PM-01_53_12
Theory : list_1
Home
Index