к
Size: a a a
2020 December 20
MK
разве в агде будет работать что-то вроде
x : (1 = 2) -> (10 = 20)
x refl = refl
?
x : (1 = 2) -> (10 = 20)
x refl = refl
?
В коке можно тактикой exfalso + inversion любую хрень доказать если в гипотезах такие равенства есть
к
В коке можно тактикой exfalso + inversion любую хрень доказать если в гипотезах такие равенства есть
ну да, тактики-то мб и могут, но они просто сгенерят построение из твоих ложных предпосылок
то есть это не магия какая-то
то есть это не магия какая-то
MK
нет такого экстеншена же ещё?
IK
нет такого экстеншена же ещё?
+
MP
А в чем реальная разница между LTS и nightly на стекежде? И то и другое снапшоты, в чем там long time support заключается?
к
1. может прикол в том, что lts у многих может быть +- одинаковый, и зависимости закэшируются, а найтли у каждого может быть свой
2. https://github.com/commercialhaskell/stackage/blob/master/MAINTAINERS.md#lts-package-guarantees-and-exceptions
вот тут написано, что у nightly версии повыше могут быть, но я не уверен что понял. Но там в целом описаны пару отличий в целях lts и nightly (второй стермится использовать самый последний ghc какой может)
2. https://github.com/commercialhaskell/stackage/blob/master/MAINTAINERS.md#lts-package-guarantees-and-exceptions
вот тут написано, что у nightly версии повыше могут быть, но я не уверен что понял. Но там в целом описаны пару отличий в целях lts и nightly (второй стермится использовать самый последний ghc какой может)
AV
А в чем реальная разница между LTS и nightly на стекежде? И то и другое снапшоты, в чем там long time support заключается?
Тем что баги дольше чинятся
MP
видимо самое существенное, что из LTS пакет не может исчезнуть
MP
Тем что баги дольше чинятся
тоже хорошо!
AV
Хотя если честно они никогда в конкретной версии не чинятся
AA
А в чем реальная разница между LTS и nightly на стекежде? И то и другое снапшоты, в чем там long time support заключается?
разницы нет