V
Size: a a a
ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
453 membersпожаловаться на группу
2019 December 13
AG
Неплохо.
надо кстати как раз портануть эти две главы для тренировки
AT
надо кстати как раз портануть эти две главы для тренировки
На что хочешь портировать? На Идрис?
AT
Чем больше рассказываю про использование пруверов, тем больше хочется это делать на белой доске. Правда, например, проверять руками доказательства студентов/слушателей совсем не хочется. Хочу такой интерфейс к Coq, чтобы распознавал писанину и транслировал в код
2019 December 14
λ
Oℕ
да
извините, наш подход всё-таки предполагать просто автовычислимую структуру в контексте, а не заставлять юзера руками мапку заполнять
Oℕ
Если вы очень хотите заполнять мапку, сделать это очень просто, можем добавить
Oℕ
Но хотелось бы хотя бы один юзкейз
Oℕ
Чем больше рассказываю про использование пруверов, тем больше хочется это делать на белой доске. Правда, например, проверять руками доказательства студентов/слушателей совсем не хочется. Хочу такой интерфейс к Coq, чтобы распознавал писанину и транслировал в код
Наконец машинлёрнинг пригодится в типах
AG
На что хочешь портировать? На Идрис?
ну да, sf in idris же
AG
Наконец машинлёрнинг пригодится в типах
пруф майнинг уже относительно давно есть
Oℕ
пруф майнинг уже относительно давно есть
Он где-то, кроме изабель юзается?
w
welcometotheclubbuddy in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Он где-то, кроме изабель юзается?
Эх, сча бы юзается?
Oℕ
Эх, сча бы юзается?
Ооооо, бот научился глагол отщеплять
w
welcometotheclubbuddy in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Ооооо, бот научился глагол отщеплять
Эх, сча бы отщеплять
AG
Он где-то, кроме изабель юзается?
для кока вроде что-то делали
V
йопта я почти в первый класс пошел
Пиздец ты старый, дядь