AT
В докладе Dotty упоминалась
Size: a a a
ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
453 membersпожаловаться на группу
2019 December 20
AT
Но, это видимо не скоро будет. Он вчера защитил диссер и кто его знает как все пойдёт дальше
GP
Grigory Pomadchin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Грустно, что нельзя считать все эти языки подмножествами кока
Када я коком маялся, точно помню что на главной странице было написано что coq implements higher level language called Gallina which is based on the calculus of inductive constructions; кок тип не название языка но именно среды название
GP
Grigory Pomadchin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Недавно был митинг кок девов, был там и Джо Бакуни, собирается в экстрактор Кока вмержить Скалу
Ничоси
AT
Aλeksei Tereχin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Недавно был митинг кок девов, был там и Джо Бакуни, собирается в экстрактор Кока вмержить Скалу
на тверской?
AT
Aλeksei Tereχin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
я буду сувать рандомные реплики
Oℕ
Када я коком маялся, точно помню что на главной странице было написано что coq implements higher level language called Gallina which is based on the calculus of inductive constructions; кок тип не название языка но именно среды название
Нет никакого противоречия в том, что есть фрейм язык, включающий несколько своих подмножеств (тавтология)
V
на тверской?
вмержил кок на тверской
AT
Aλeksei Tereχin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
прошивка биоса помогла. держу в курсе
GP
Grigory Pomadchin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Нет никакого противоречия в том, что есть фрейм язык, включающий несколько своих подмножеств (тавтология)
как скажешь, к словам придираюсь; не видел чтоб использовали coq is a language
AT
как скажешь, к словам придираюсь; не видел чтоб использовали coq is a language
Бывает, но скорее в разговорной речи, чем на письме
GP
Grigory Pomadchin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
Бывает, но скорее в разговорной речи, чем на письме
так - видел
Oℕ
Если есть целостный кусок текста и процедура по его парсингу и тайпчеку, включащем парсинг, интерпретацию и тайпчек одновременно нескольких языков, полагаю, стоит говорить о наличии некоторого обощающего языка
AT
.v файлы это по сути скрипты для репла
GP
Grigory Pomadchin in ПОКА ОДЕРСКИ НЕ ВИДИТ (наш M.D. (потому что его нет. нельзя увидеть то, чего нет.))
это скорее компилятор
Oℕ
А где "Кок - это язык доказательств с зависимыми типами", "Изоморфизм Карри-Говарда обнаружили Карри и Говард", "Если применить функцию A -> B к A получим B"
Но понятно, что к этой реплике придираться очень тупо, потому что это пересказ квновской шутки, а не высказывание о материале