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 :
spread: spread def,
and: P ∧ Q,
equal: s = t ∈ T,
int: ℤ,
copath-length: copath-length(p)
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:
2019_06_20-PM-00_57_59
Last ObjectModification:
2019_01_02-PM-01_34_36
Theory : co-recursion-2
Home
Index