Nuprl Definition : bar-converges
x↓a == ∃n:ℕ. (bar-val(n;x) = (inl a) ∈ (T?))
Definitions occuring in Statement :
bar-val: bar-val(n;x),
nat: ℕ,
exists: ∃x:A. B[x],
unit: Unit,
inl: inl x,
union: left + right,
equal: s = t ∈ T
Definitions occuring in definition :
exists: ∃x:A. B[x],
nat: ℕ,
equal: s = t ∈ T,
union: left + right,
unit: Unit,
bar-val: bar-val(n;x),
inl: inl x
FDL editor aliases :
bar-converges
Latex:
x\mdownarrow{}a == \mexists{}n:\mBbbN{}. (bar-val(n;x) = (inl a))
Date html generated:
2016_05_14-AM-06_20_07
Last ObjectModification:
2015_09_22-PM-05_47_38
Theory : co-recursion
Home
Index