KL
Kirill Shelopugin
https://scastie.scala-lang.org/3OPb9v2MQdqf2HZTUHYdbg
Деструктуризация, видимо
Деструктуризация, видимо
Не, это будет работать, да
Size: a a a
2020 December 06
NL
Ух блин! А есть ещё?
KL
Вопрос в том, почему нейминг параметр пролезает в скоуп
V
@aleksei_t добавьте в стикерпак
R
в обязательном порядке
нужен спинофф понва, зарегистрированный в ВАК
Пока Одерски Не Видит Как Мы Рецензируем
нужен спинофф понва, зарегистрированный в ВАК
Пока Одерски Не Видит Как Мы Рецензируем
сук
KL
Kirill Shelopugin
https://scastie.scala-lang.org/3OPb9v2MQdqf2HZTUHYdbg
Деструктуризация, видимо
Деструктуризация, видимо
Более того, если таки добавить тип, то компиляция пройдет
AT
Vasiliy
@aleksei_t добавьте в стикерпак
Ок
V
принял
NL
иногда формализация даже подсказывает как нужно теорию строить
Антон, можно ли обобщить чего-нибудь так, чтобы с лёгкостью переиспользовать в разных доказательствах. Например, диагональный метод Кантора используется и при доказательстве несчётности действительных чисел, и при доказательстве несуществования универсальной МТ, и (кажется) при доказательстве теоремы Гёделя.
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
w
Антон, можно ли обобщить чего-нибудь так, чтобы с лёгкостью переиспользовать в разных доказательствах. Например, диагональный метод Кантора используется и при доказательстве несчётности действительных чисел, и при доказательстве несуществования универсальной МТ, и (кажется) при доказательстве теоремы Гёделя.
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
Не читаемо в текстовом виде.
NL
Не читаемо в текстовом виде.
Может надо рисунок фотографии скриншота?
AT
Антон, можно ли обобщить чего-нибудь так, чтобы с лёгкостью переиспользовать в разных доказательствах. Например, диагональный метод Кантора используется и при доказательстве несчётности действительных чисел, и при доказательстве несуществования универсальной МТ, и (кажется) при доказательстве теоремы Гёделя.
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
Интуитивно кажется, что можно это обобщить как-нибудь и потом переиспользовать уже в частных доказательствах.
Индукцию, как я понимаю, вполне успешно переиспользуют практически везде, нет?
если говорить про док-ва на тактиках, то обычно тут либо на уровне метода переиспользование (мета-мета-уровень), либо на мета-уровне "универсальные" пруф-скрипты пишутся.
Тот же Chlipala известен такими вещами. У него есть знаменитая тактика
Тот же Chlipala известен такими вещами. У него есть знаменитая тактика
crush. С ее помощью часто док-ва превращаются во что-то типа induction x; crush.AT
с другой стороны вещи типа диагонального метода встречаются довольно редко
R
может еще не доросли до такого?
NL
с другой стороны вещи типа диагонального метода встречаются довольно редко
Ок, ок. Спасибо за ответ.