May. 28th, 2013

akuklev: (Свечка и валокардин)
Заметил за собой, что в результате воздействия на моск зависимых теорий типов совсем перестал использовать при записи кванторы. Пишу в конспектах и на бумажках в таком вот духе:
(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]
)

December 2016

S M T W T F S
    123
456789 10
11121314151617
18192021222324
25262728293031

Page Summary

Style Credit

Expand Cut Tags

No cut tags
Page generated Sep. 21st, 2025 06:24 am
Powered by Dreamwidth Studios