Nuprl Definition : copath-last
copath-last(w;p) ==
if (copath-length(p) =z 1) then <w, copath-hd(p)> else copath-last(coW-item(w;copath-hd(p));copath-tl(p)) fi
Definitions occuring in Statement :
copath-tl: copath-tl(x),
copath-hd: copath-hd(p),
copath-length: copath-length(p),
coW-item: coW-item(w;b),
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
pair: <a, b>,
natural_number: $n
Definitions occuring in definition :
ifthenelse: if b then t else f fi ,
eq_int: (i =z j),
copath-length: copath-length(p),
natural_number: $n,
pair: <a, b>,
coW-item: coW-item(w;b),
copath-hd: copath-hd(p),
copath-tl: copath-tl(x)
FDL editor aliases :
copath-last
Latex:
copath-last(w;p) ==
if (copath-length(p) =\msubz{} 1)
then <w, copath-hd(p)>
else copath-last(coW-item(w;copath-hd(p));copath-tl(p))
fi
Date html generated:
2019_06_20-PM-00_56_44
Last ObjectModification:
2019_01_02-PM-01_33_48
Theory : co-recursion-2
Home
Index