Nuprl Definition : code-seq1
code-seq1(k;s) == primrec(k;0;λi,x. if (i =z 0) then s i else code-pair(x;s i) fi )
Definitions occuring in Statement :
code-pair: code-pair(a;b),
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
apply: f a,
lambda: λx.A[x],
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
lambda: λx.A[x],
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
natural_number: $n,
code-pair: code-pair(a;b),
apply: f a
FDL editor aliases :
code-seq1
Latex:
code-seq1(k;s) == primrec(k;0;\mlambda{}i,x. if (i =\msubz{} 0) then s i else code-pair(x;s i) fi )
Date html generated:
2016_05_15-PM-05_22_11
Last ObjectModification:
2015_09_23-AM-07_53_37
Theory : general
Home
Index