CD
в/на Донбасс, где никель, марганец и т.д.?
да, УССР в 1940 была несколько до Киева
Size: a a a
2020 August 30
P
да, УССР в 1940 была несколько до Киева
я про то, что чермету нужны некоторые руды, которых на Донбассе залежи
CD
я про то, что чермету нужны некоторые руды, которых на Донбассе залежи
а я про то, что РИ в 1910 году в абсолютных числах таки обогнала Бельгию
CD
а черт
CD
я смотрю сталь а не чугун в 1940
CD
P
потому там можно штамповать
p
emptyIsSuffixAlways : (Eq a) => (xs : List a) -> isSuffix [] xs = True
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
@Psilon вот как нужно продвигать верификацию. как замену тестам)
p
то есть пишешь в стиле тестов только леммы
p
большую часть в итоге за тебя доказывает сам идрис а ты тупо Refl пишешь
P
а рф большая, но разбитая и малообжитая, построение магистралей и освоение ебеней рабским трудом смогло повысить производство руды в совке
NL
NL
H
H
недалеко от истины
P
emptyIsSuffixAlways : (Eq a) => (xs : List a) -> isSuffix [] xs = True
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
тесты, ток в тестах тоже бывают ошибки. кто проверит твои леммы?
p
тесты, ток в тестах тоже бывают ошибки. кто проверит твои леммы?
леммы никто кроме тебя не может проверить
P
леммы никто кроме тебя не может проверить
именно, потому чтоб продвигать их, надо продвигать тестирование требований
H
emptyIsSuffixAlways : (Eq a) => (xs : List a) -> isSuffix [] xs = True
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
Будет чуточку легче, если называть леммы по-нормальному
p
именно, потому чтоб продвигать их, надо продвигать тестирование требований
прикол верификации что ошибку ты можешь допустить ТОЛЬКО в написании леммы