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 :
copath-tl: copath-tl(x),
copath-hd: copath-hd(p),
coW-item: coW-item(w;b),
pair: <a, b>,
natural_number: $n,
copath-length: copath-length(p),
eq_int: (i =z j),
ifthenelse: if b then t else f fi
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:
2018_07_25-PM-01_40_31
Last ObjectModification:
2018_07_24-AM-09_34_31
Theory : co-recursion
Home
Index