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