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 :
apply: f a,
code-pair: code-pair(a;b),
natural_number: $n,
eq_int: (i =z j),
ifthenelse: if b then t else f fi ,
lambda: λx.A[x],
primrec: primrec(n;b;c)
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:
2019_06_20-PM-02_39_33
Last ObjectModification:
2019_06_12-PM-00_27_41
Theory : num_thy_1
Home
Index