(no subject)

Заметил за собой, что в результате воздействия на моск зависимых теорий типов совсем перестал использовать при записи кванторы. Пишу в конспектах и на бумажках в таком вот духе:

(a: Int, b: Int) ⇒ [a + b = b + a]
(a: Int) ⇒ (b: Int, [a + b = 0])

Или, когда посложнее,

(X: UniformSpace,
 Y: UniformSpace,
 f: X ⇒Cont Y,
 p0: X,
 eps: Y.Distance)
⇒
(delta: X.Distance,
  (p: X, [dist(p, p0) < eps])
  ⇒
  [dist(f(p), f(p0)) < eps]
)