Nuprl Definition : coPath-at

coPath-at(n;w;p) ==  if (n =z 0) then w else let t,q = p in coPath-at(n - 1;coW-item(w;t);q) fi 


Definitions occuring in Statement :  coW-item: coW-item(w;b),  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spread: spread def,  subtract: n - m,  natural_number: $n
Definitions occuring in definition :  ifthenelse: if b then t else f fi ,  eq_int: (i =z j),  spread: spread def,  subtract: n - m,  natural_number: $n,  coW-item: coW-item(w;b)
FDL editor aliases :  coPath-at
Latex:
coPath-at(n;w;p)  ==    if  (n  =\msubz{}  0)  then  w  else  let  t,q  =  p  in  coPath-at(n  -  1;coW-item(w;t);q)  fi 


Date html generated: 2019_06_20-PM-00_56_15
Last ObjectModification: 2019_01_02-PM-01_33_05

Theory : co-recursion-2


Home Index