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 :  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
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: 2019_06_20-PM-00_56_19
Last ObjectModification: 2019_01_02-PM-01_33_08

Theory : co-recursion-2


Home Index