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 :
coW-item: coW-item(w;b),
natural_number: $n,
subtract: n - m,
spread: spread def,
eq_int: (i =z j),
ifthenelse: if b then t else f fi
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:
2018_07_25-PM-01_38_28
Last ObjectModification:
2018_07_18-PM-05_16_22
Theory : co-recursion
Home
Index