P
это построено в 41-43 годах
и?
Size: a a a
2020 August 30
P
я всё ещё не понимаю о чём ты
CD
и?
эммм.... как бы тебе объяснить
P
(и я не думаю, что в 41-43х было построено это ВСЁ, как минимум, там изначально была куча бараков, на месте которых уже позже возвели полноценное жильё)
CD
(и я не думаю, что в 41-43х было построено это ВСЁ, как минимум, там изначально была куча бараков, на месте которых уже позже возвели полноценное жильё)
ВСЁ
ΑZ
@Psilon вот как нужно продвигать верификацию. как замену тестам)
я 100 раз это говорил
ΑZ
но не слушають
ΑZ
emptyIsSuffixAlways : (Eq a) => (xs : List a) -> isSuffix [] xs = True
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
emptyIsSuffixAlways xs = Refl
смотрите, а чем леммы не тесты?
только мне не нравится = True, но мб это мои проблемы
p
только мне не нравится = True, но мб это мои проблемы
а как по другому?
H
@Psilon вот как нужно продвигать верификацию. как замену тестам)
Нет, это бесполезно, не слушают
ΑZ
а как по другому?
ну обычно это в типах лежит
ΑZ
посмотри на GTE в Nat.idr например
p
ну обычно это в типах лежит
ну хз я намакакил и все
CD
вот это остальная самара до них
ΑZ
они могли сделать a <= b = True, но отдельный типчик лучше
p
кстати я попытался выразить неправильную лемму, и у меня сигнатура не скомпилировалась, лол
ΑZ
кстати я попытался выразить неправильную лемму, и у меня сигнатура не скомпилировалась, лол
мы это уже проходили на примере суффикса списка)
ΑZ
затем завтипы и нужны, чтобы говно не компилялось
p
мы это уже проходили на примере суффикса списка)
я вот тоже на суффиксе