Nuprl Definition : pcw-path-coPath
pcw-path-coPath(n;p) ==
if (n =z 0)
then ()
else let param,w',d = p (n - 1) in
case d
of inl(b) =>
let pp = pcw-path-coPath(n - 1;p) in
if (copath-length(pp) =z n - 1) then copath-extend(pp;b) else () fi
| inr(x) =>
()
fi
Definitions occuring in Statement :
copath-nil: ()
,
copath-length: copath-length(p)
,
copath-extend: copath-extend(q;t)
,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
let: let,
spreadn: spread3,
apply: f a
,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
,
subtract: n - m
,
natural_number: $n
Definitions occuring in definition :
spreadn: spread3,
apply: f a
,
decide: case b of inl(x) => s[x] | inr(y) => t[y]
,
let: let,
ifthenelse: if b then t else f fi
,
eq_int: (i =z j)
,
copath-length: copath-length(p)
,
subtract: n - m
,
natural_number: $n
,
copath-extend: copath-extend(q;t)
,
copath-nil: ()
FDL editor aliases :
pcw-path-coPath
Latex:
pcw-path-coPath(n;p) ==
if (n =\msubz{} 0)
then ()
else let param,w',d = p (n - 1) in
case d
of inl(b) =>
let pp = pcw-path-coPath(n - 1;p) in
if (copath-length(pp) =\msubz{} n - 1) then copath-extend(pp;b) else () fi
| inr(x) =>
()
fi
Date html generated:
2019_06_20-PM-00_56_58
Last ObjectModification:
2019_01_02-PM-01_34_09
Theory : co-recursion-2
Home
Index