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