Nuprl Definition : code-seq1

code-seq1(k;s) ==  primrec(k;0;λi,x. if (i =z 0) then else code-pair(x;s i) fi )



Definitions occuring in Statement :  code-pair: code-pair(a;b) primrec: primrec(n;b;c) ifthenelse: if then else fi  eq_int: (i =z j) apply: a lambda: λx.A[x] natural_number: $n
Definitions occuring in definition :  apply: a code-pair: code-pair(a;b) natural_number: $n eq_int: (i =z j) ifthenelse: if then else 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