Nuprl Definition : coPath-extend

coPath-extend(n;p;t) ==  if (n =z 0) then <t, ⋅> else let x,y = p in <x, coPath-extend(n - 1;y;t)> fi 


Definitions occuring in Statement :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  it: ⋅,  spread: spread def,  pair: <a, b>,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  natural_number: $n,  subtract: n - m,  pair: <a, b>,  spread: spread def,  it: ⋅,  eq_int: (i =z j),  ifthenelse: if b then t else f fi 
FDL editor aliases :  coPath-extend
Latex:
coPath-extend(n;p;t)  ==
    if  (n  =\msubz{}  0)  then  <t,  \mcdot{}>  else  let  x,y  =  p  in  <x,  coPath-extend(n  -  1;y;t)>  fi 


Date html generated: 2018_07_25-PM-01_38_36
Last ObjectModification: 2018_07_18-PM-07_00_56

Theory : co-recursion


Home Index