Nuprl Definition : coW-pos-lens
coW-pos-lens(p;i;j) == let u,v = p in (copath-length(u) = i ∈ ℤ) ∧ (copath-length(v) = j ∈ ℤ)
Definitions occuring in Statement :
copath-length: copath-length(p),
and: P ∧ Q,
spread: spread def,
int: ℤ,
equal: s = t ∈ T
Definitions occuring in definition :
copath-length: copath-length(p),
int: ℤ,
equal: s = t ∈ T,
and: P ∧ Q,
spread: spread def
FDL editor aliases :
coW-pos-lens
Latex:
coW-pos-lens(p;i;j) == let u,v = p in (copath-length(u) = i) \mwedge{} (copath-length(v) = j)
Date html generated:
2018_07_25-PM-01_42_51
Last ObjectModification:
2018_06_16-AM-09_39_04
Theory : co-recursion
Home
Index