Dmitry [Shep]
Anonymous
Привет, чят. Мы тут в соседнем окне телеграм обсуждали, и мне дали ссылку на этот чат, а у меня как раз релевантный вопрос возник.
ARTi
Anonymous
Короче, я читаю книгу Certified Programming with Dependent Types, и там в главе 14.2 почти в самом конце приводится пример
Theorem t1' : forall x: nat, x = x.
match goal with
| [ |- forall x, ?P ] => trivial
end.
Мол, из-за явной привязки предиката это не должно работать, так как P будет ссылаться на забаунденную переменную x. Однако, в моей версии Coq (8.9.1) всё работает, и если написать вместо trivial, например, idtac P, то я получу (x = x). В новом коке что-то существенно изменилось, или дело в чём-то другом?
Нехис
а сперва показался приличным и адекватным
Anonymous
:(
Aragaer
это надо в какой-нибудь хаскелчатик, а там уже спросить, куда дальше пройти
Нехис
Aragaer
но люди, которые там сидят, подскажут, в каком чатике они говорят про эти абстрактные материи
Aragaer
ну понятно же, что это не в чатик по теории категорий
Anonymous
Ну можно обсуждать категориальную семантику различных теорий типов.
Anonymous
Правда, я в этом пока не шарю особо.
Alex
не то чтобы мы тебя выгоняем) но тут ты вряд ли найдешь ответ
☕️ Паша ☭👨🏻🔧
whenever... wherever.... 42 is the correct answer.
Анатолий
Ну пока хаскеллисты не обнаружились. Могут и быть, а могут и не быть тут) лучше и правда сразу в профильный пойти
ARTi
У меня не нормально. Сертификаты для хттпс не работают же.
ARTi
У меня если слетает то в 2010 вроде
Space
Настрой правильно часовой пояс)
Space
Может и из-за батареи быть, да:)
Andrey
Ну так 6 часов - это фигня. У сертов время жизни от нескольких месяцев до нескольких лет.
Анатолий
Анатолий
Вроде собирались в хроме сделать специальную предупреждалку, когда у юзера часы бегут
Анатолий
Но хз сделали или нет
Анатолий
Andrey
При 6 часах смещения, даже если серту еще жить год?
Анатолий
Andrey
А в чем?
Andrey
Хм, надо будет проверить...
Анатолий
А в чем?
Точно не знаю, но это другая ошибка
Анатолий
SEC_ERROR_OCSP_FUTURE_RESPONSE
Анатолий
а то SEC_ERROR_EXPIRED_CERTIFICATE
Andrey
Ну хз, поставил себе 23:48, на андроиде хром нормально открыл гугл.ком
Анатолий
Что-то типа что ответ из будущего ещё не действителен, потому что содержит дату из будущего
Анатолий
Деталей не знаю
Aragaer
родное китайское?
Анатолий
OH WAIT 😁
Space
Сейчас дисплеи сильно подешевели, даже фуллхд
Space
Правда без жирофоба, с ним дороже весьма)
ARTi
Линыч
А смысл, если защитное стекло поверх..?👀
Линыч
Ну пися ну ты чего
Линыч
Даже не знаю, почему.
Space
Space
☕️ Паша ☭👨🏻🔧
Caterpillar S60. Ни стекла, ни чехол не нужны. Плёнка с завода и всё.
Alex
он с тепловизором по моему еще
☕️ Паша ☭👨🏻🔧
Угу ;-)
☕️ Паша ☭👨🏻🔧
Но пришлось под себя, допилить. Рут + софт и магнитную зарядку.
Alex
как тепловизор? полезно?
☕️ Паша ☭👨🏻🔧
Alex
а в практическом плане используешь?
Beardy
Думал у него похуже с дальностью.
ARTi
☕️ Паша ☭👨🏻🔧
☕️ Паша ☭👨🏻🔧
Мне дня два. Но можно и за пол дня ушатать.
☕️ Паша ☭👨🏻🔧
Пользую довольно часто, в основном по работе. Только жалею, что просто смотрю, а фото делать забываю. Иногда бывает очень наглядно и красиво.
☕️ Паша ☭👨🏻🔧
На этой неделе нашли остатки прозрачного флюса с сопротивлением и дроссель в перенасыщении.
ARTi
выбираю настольную лампу для учебы, такая норм ребят? https://market.yandex.ru/product--nastolnaia-lampa-xiaomi-philips-eyecare-smart-lamp-2/439476046?show-uid=15709929997100084408816001&nid=55153&context=search
☕️ Паша ☭👨🏻🔧
Всё зависит от того какой в неё special ability вставлена и сколько она плюс даёт обучаемости.
Линыч
Любая лампа, в которую можно вкрутить икеевскую лампочку на 1000люменов и вперёд
ARTi
ARTi
Любая лампа, в которую можно вкрутить икеевскую лампочку на 1000люменов и вперёд
https://www.ikea.com/ru/ru/p/ledare-svetodiod-e27-1000-lm-reguliruemaya-yarkost-teplyy-reguliruemaya-yarkost-sharoobraznyy-molochnyy-10363298/?gclid=EAIaIQobChMIsNDB4PGy5QIVAqmaCh2VnwihEAQYASABEgLwN_D_BwE&utm_campaign=ipr_Msk_smart-shopping_all&utm_content=tid|pla-293946777986|cid|1932699969|aid|350439015315|gid|70590954957|pos||src|u_|dvc|c|reg|9047068|rin|&utm_medium=cpc&utm_source=google&utm_term=
ARTi
эта?
ARTi
не могу найти питер в сайте икеи
Павел
Павел
Павел
Хотя дохнет как и любая другая.
ARTi
Павел
как быстро?
Год - два. Опять же от качества проводки зависит
ARTi
Павел
Можно и медную плохо кинуть.
Павел
ARTi
ARTi
ARTi
у меня в квартире когда работает микроволновка и включаю чайник, ощущение что микроволновка звук меняет, ничего страшного?
Павел
а что за проблема?
У них диэлектрическая пара возникает и место соединения очень греется