(no subject)
May. 28th, 2013 01:38 pmЗаметил за собой, что в результате воздействия на моск зависимых теорий типов совсем перестал использовать при записи кванторы. Пишу в конспектах и на бумажках в таком вот духе:
Или, когда посложнее,
(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] )