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