Вариант для распечатки		Пред. тема | След. тема
Форум Разговоры, обсуждение новостей
Режим отображения отдельной подветви беседы		[ Отслеживать ]

Инструментарий для доказательства теорем Coq рассматривает возможность смены названия, opennews (??), 09-Апр-21, (0) [смотреть все] Зачем эта очень важная новость нужна именно на опеннете , Hedgehog (??), 23:22 , 09-Апр-21, (1) +9 // чтобы ты был в курсе, как мир сходит с ума, подстраиваясь под англицизмы, Антифрактал (?), 23:23 , 09-Апр-21, (6) +24 // Вернее подстраиваясь под впечатлительных подростков, феминисток, гомосеков и про, Аноним (23), 00:27 , 10-Апр-21, (23) +19 // анон, ну не смешно вообще Если ьы он назывался hui - у нас бы точно так же измы, Аноним (82), 10:01 , 10-Апр-21, (82) +2 Почему бы Пожалуйста https gethue com PS Кстати работает оно вполне соотве, RomanCh (ok), 09:50 , 11-Апр-21, (138) но истерить до смены названия не стали бы , ого (?), 19:43 , 11-Апр-21, (154) Это как с проектом pydora Где-то в тексте на PyPI можно засвидетельствовать , Wine_O_Feliya (?), 15:11 , 12-Апр-21, (161) Обидно, да Под впечатлительных подростков, феминисток и гомосеков они подстраив, Ordu (ok), 10:38 , 10-Апр-21, (88) +3 Так мы просто пошутили и посмеялись, но никто не поднимал серьезно вопрос о пере, Аноним (23), 13:42 , 10-Апр-21, (103) +7 А когда людям надоедает это хихиканье адекватных и психически здоровых при к, Ordu (ok), 15:04 , 10-Апр-21, (110) +1 Новость читал Не автору надоело хихканье, иначе он бы так не назвал А некотор, Аноним (164), 17:26 , 12-Апр-21, (164) +2 Да Адекватные и психически здоровые люди отпускали двусмысленные шутки в , Ordu (ok), 18:27 , 12-Апр-21, (169) CKEditor 8212 свободный WYSIWYG-редактор До версии 3 0 назывался FCKed, Аноним (47), 02:40 , 10-Апр-21, (47) +4 // Этот редактор такое же гуано, как и аргументы про Coq, Неа (?), 09:26 , 10-Апр-21, (81) –2 А как тебе ЁбРедактор Сколько у нас ржали над ё-мобилем Или это другое Свое к, Аноним (82), 10:03 , 10-Апр-21, (83) –2 Vi как vi, чё бухтеть- то , Noname (??), 15:52 , 13-Апр-21, (176) –1 Язык международного общения - английский Не китайский и не русский как некоторы, Аноним (59), 06:47 , 10-Апр-21, (59) // Однако, в основном, только носители этого недоязыка понимают эту игру слов Я во, Тот_Самый_Анонимус (?), 06:56 , 10-Апр-21, (63) +14 Про китайский - согласен, хотя это больше дело будущего А на русском ты разве чт, myhand (ok), 07:37 , 10-Апр-21, (68) –2 Нет В ООН на самом деле тоже можно https www un org ru sections about-un off, RomanCh (ok), 09:54 , 11-Апр-21, (139) +1 Ну, ООН - известна своей научностью Там даже Эйлер состоял Нет, вру Эйлер в , myhand (ok), 12:15 , 11-Апр-21, (144) –1 Уууу Понятно , RomanCh (ok), 12:44 , 11-Апр-21, (147) +1 и 7 лайкосов Как грица угадай в какой стране живут нацисты, расисты и шовинисты , Аноним (82), 10:04 , 10-Апр-21, (84) –1 Во всех К сожалению Но вообще про проблемы английского я в целом согласен, в си, RomanCh (ok), 09:57 , 11-Апр-21, (140) А зачем с этим что-то делать Есть эсперанто , myhand (ok), 12:16 , 11-Апр-21, (145) И как у вас с ним Регулярно практикуете Научные статьи в мухосранскую академию, RomanCh (ok), 12:45 , 11-Апр-21, (148) +1 - Ты же робот, имитация жизни Может робот способен написать симфонию - Будто ты, Noname (??), 15:56 , 13-Апр-21, (177) Какой вы агрессивный, батенька Будем лечиться Смирительную рубашку на него Та, Доктор психушки (?), 17:59 , 12-Апр-21, (166) А что не так , Noname (??), 15:58 , 13-Апр-21, (178) Чувачок, тебе реально нужно как минимум успокоительного попить Когда везде мере, Аноним (164), 18:02 , 12-Апр-21, (167) Чтобы через Интерпол его экстрадировать в РФ и посадить здесь в тюрьму за оскорб, Аноним (57), 06:02 , 10-Апр-21, (57) –2 // есть мнение, что НИКАКОЕ название не пройдет через такую нейросеть везде будет з, СеменСеменыч777 (?), 15:41 , 10-Апр-21, (111) // СеменСеменыч777 бы не прошел прежде всего в СССР, ежели бы тот не распался По, Аноним (82), 06:57 , 11-Апр-21, (127) Ну а при каком обстоятельстве посетители opennetу впринципе могли бы узнать, что, myhand (ok), 06:54 , 10-Апр-21, (61) // Ради красного словца не пожалеем и отца Разумеется подтверждения своим словм вы, Тот_Самый_Анонимус (?), 06:59 , 10-Апр-21, (64) +2   // Ну, представленного общественности инструмента уровня Coq разработано было не бы, myhand (ok), 07:06 , 10-Апр-21, (66)   Слава морфу Слава 404 Защифрованное послание, которое поймут лишь избранные , НеОН (?), 17:23 , 12-Апр-21, (163) +1 Hey bro nice Coq, Аноним (2), 23:22 , 09-Апр-21, (2) +16 // Nice coq, awesome balls terminator jpg, Аноним (-), 02:43 , 10-Апр-21, (48) +1 https derpicdn net img view 2021 4 2 2584442__safe_artist-colon-handgunboi_pri, iPony129412 (?), 07:04 , 10-Апр-21, (65) –1 Nice coq, swesome proofs , Человек под травой (?), 09:25 , 10-Апр-21, (80) Gallina blank a bool bool, Wine_O_Feliya (?), 15:13 , 12-Апр-21, (162) Одобряю Но только если они знали о проблеме с названием, почему назвали язык то, Аноним (3), 23:22 , 09-Апр-21, (3) –4 // А они в качестве шутки тогда и сделали такое название Но то было тогда а сейча, Аноним (18), 23:58 , 09-Апр-21, (18) +8 // Потому что этот Терри совершенно не парится что кто-то на слух воспримет его фам, пох. (?), 09:21 , 10-Апр-21, (78) No fun allowed , Тётка с ведром (?), 10:43 , 10-Апр-21, (89) французы, сэр Тогда постебались, а теперь боязно стало , Cradle (?), 00:35 , 10-Апр-21, (25) Coq - петух с франц Раньше было модно-молодёжно по дурацки именовать продукт Н, Lex (??), 04:30 , 10-Апр-21, (56) –2 // А фамилию им тоже выросши внезапно сменить А то ж вызывает нездоровые ассоциаци, пох. (?), 09:22 , 10-Апр-21, (79) +2 лол блин Ты правда считаешь что петух имеет негативную коннотацию во Франции П, Аноним (82), 10:10 , 10-Апр-21, (85) +1 // Я лишь говорю, что кок - петух с французского И что раньше была мода черти как , Lex (??), 13:58 , 10-Апр-21, (104) +1 Вот ты можешь по названию проги - 171 Windows 187 , однозначно догадаться что, Аноним (82), 07:01 , 11-Апр-21, (128) +2 Окна экраны Какая-то взаимосвязь естьink - чернила Есть какая-то связь с рис, Lex (??), 14:42 , 11-Апр-21, (151) Мнэээ Вы точно с собой дискутировали , Michael Shigorin (ok), 21:25 , 11-Апр-21, (157) +1 Заранее ответил, предвидя очередной тупой вопрос в продолжение не мене тупого ср, Lex (??), 11:21 , 12-Апр-21, (160) Вообще, FYI, петух во франции - это почти что национальный маскот , InuYasha (??), 11:33 , 11-Апр-21, (143) +2 Представляю, как сейчас краснеет в гробу Джобс со своим ха ЯБЛОКОМ , Gogi (??), 11:39 , 10-Апр-21, (92) –2 Пропиарились же , Аноним (57), 06:04 , 10-Апр-21, (58) +1 Потому что в основу Coq положена теория типов calculus of constructions CoC , Аноним (97), 12:28 , 10-Апр-21, (97) +2 При всем этом остается загадка как до сих пор не сломлен ГИМП , Аноным (ok), 23:22 , 09-Апр-21, (4) +7 // Глимпс, Аноним (7), 23:23 , 09-Апр-21, (7) –1 // Не существует , Стас Михайлов (?), 23:51 , 09-Апр-21, (17) +5 Глиномес FTGJFIX, Аноним (74), 08:51 , 10-Апр-21, (74) +1 Прокудин им не дает сломаться, поит их воткой Это стимулирует их моск посылать , Антифрактал (?), 23:24 , 09-Апр-21, (8) +5 // Слава Прокудину , Annoynymous (ok), 23:31 , 09-Апр-21, (10) +2 // Прокудину слава , Аноним (26), 01:07 , 10-Апр-21, (26) Андрей, Аноним (41), 02:01 , 10-Апр-21, (41) https www opennet ru opennews art shtml num 51357https www opennet ru openne, Аноним (-), 23:31 , 09-Апр-21, (11) +1 // Форк же, а не переименован, Аноным (ok), 23:59 , 09-Апр-21, (19) +1 Язык Си - первая буква слова cock , Аноним (7), 23:22 , 09-Апр-21, (5) +5 // А rust от ruster - кугут, Жорш (?), 01:18 , 10-Апр-21, (33) +1 // Давненько не слышал этого слова , Какаянахренразница (ok), 11:26 , 10-Апр-21, (91) Я прозрел, Аноним (34), 01:19 , 10-Апр-21, (34) +3 Думаю, низкосортный вообще и сортирный в частности юмор существовал и раньше , Q2W (?), 08:10 , 10-Апр-21, (70) +5 Если стеблись, когда называли, то надо продолжать в том же духе Если у кого-то , timur.davletshin (ok), 23:32 , 09-Апр-21, (12) +6 // Например, можно назвать 960 dr , Аноним (21), 00:10 , 10-Апр-21, (21) Потому что небритые цветноволосые ненавидят всё, что связано с мущщинками , Аноним (26), 01:10 , 10-Апр-21, (27) // вообще не врубаешься Сидят двое коллег пишут доказательства парень, девушка П, Аноним (82), 10:14 , 10-Апр-21, (86) –2 // Когда-то в очередной раз сдавал лабу по туннельному эффекту, а наш поток безуспе, n00by (ok), 11:26 , 10-Апр-21, (90) +2 тетка в теме чтобы сдать лабу - надо отсосать , Михрютка (ok), 14:12 , 10-Апр-21, (105) Есть такая штука - шприц для удаления припоя, он же вакуумный оловоотсос, в прос, n00by (ok), 07:25 , 11-Апр-21, (133) +2 Ж , Аноним (82), 07:04 , 11-Апр-21, (129) Анатомию иди отмени Там не только названия, но и картинки показывают неприличны, Аноним (98), 12:47 , 10-Апр-21, (98) +2 уже ж отменили точнее, пытались https kulturomania ru news item kommunisty-, пох. (?), 11:03 , 12-Апр-21, (159) Какая надуманная ситуация Я девушка-программист, и 1 никогда такого рода шутки , Аноним (164), 18:20 , 12-Апр-21, (168) +2 ты бы, конечно, предпочёл, чтобы это были два парня, да , ого (?), 18:56 , 12-Апр-21, (170) Вот же неженки блин, бабу коком напугали Толи наши люди, ковыряются в Zope молч, Аноним (45), 02:23 , 10-Апр-21, (45) +4 // Так там же уже Grok или что там , Аноним (82), 10:15 , 10-Апр-21, (87) А представьте когда такие проблемы надо будет разруливать авторам учебников и по, Ag (ok), 08:31 , 10-Апр-21, (71) // Каплун пулярка 8212 всё придумано уже , timur.davletshin (ok), 08:41 , 10-Апр-21, (73) А еще надо запретить Code Of Conduct, Аноним (13), 23:35 , 09-Апр-21, (13) +9 // CoC всегда потеха для рубиста, Жорш (?), 01:20 , 10-Апр-21, (36) Гашина - испанское слово 128540 , Аноним (15), 23:41 , 09-Апр-21, (15) Так Галина Бланка это не жена Моисея Бланка Как теперь жить , Аноним (16), 23:50 , 09-Апр-21, (16) +2 // На испанском Gallina blanca - это вообще Белая курица Попробуйте пожить с э, cz (??), 01:52 , 10-Апр-21, (39) +6 // Для Галлов петух тотемная птица, предвестник рассвета , n00by (ok), 07:45 , 10-Апр-21, (69) // Он для всех нормальных людей предвестник рассвета Кроме всяких городских озабоч, Аноним (100), 13:12 , 10-Апр-21, (100) +1 Есть версия, что галлы и славяне -- эдакая лингвистическая калька Первое ро, n00by (ok), 07:46 , 11-Апр-21, (134) задорновщина я поставил себе за правило - игнорировать любые лингвистические арг, СеменСеменыч777 (?), 09:04 , 11-Апр-21, (137) Заметно, ведь три топора - это популярное в некоторых кругах питиё советских в, n00by (ok), 07:11 , 13-Апр-21, (171) не вижу связи скорее всего её и нет ps анонимусу сменить ник - дело пяти минут, СеменСеменыч777 (?), 20:20 , 15-Апр-21, (179) я поставил себе за правило - игнорировать любые аргументы, СеменСеменыч777 (?), 10:06 , 16-Апр-21, (181) Вот это пральна - , n00by (ok), 10:07 , 16-Апр-21, (182) Но вообще правильно, слишком грубо это Наверняка все шутят постоянно Предлагаю , Аноним (18), 00:02 , 10-Апр-21, (20) +3 Предлагаю поменять на Гуч, Дихлофос (?), 00:11 , 10-Апр-21, (22) There are no easter eggs in Gallina , InuYasha (??), 00:34 , 10-Апр-21, (24) –1 // Буль-буль , Dzen Python (ok), 01:12 , 10-Апр-21, (29) –2 // М-да, у этих анонов нет чувства юмора , InuYasha (??), 11:28 , 11-Апр-21, (142) +1 Предлагаю вообще не использовать буквы любого алфавита - они все так или иначе в, Dzen Python (ok), 01:11 , 10-Апр-21, (28) –4 // Концу мир , Аноним (43), 02:21 , 10-Апр-21, (43) // Да, майн либен , Dzen Python (ok), 19:54 , 10-Апр-21, (123) +1 А миру герцог , Annoynymous (ok), 01:41 , 11-Апр-21, (126) Там это ВВС не собирается предпринимать срочные меры , Аноним (26), 01:12 , 10-Апр-21, (30) +5 Да Правильно Кок это как бы лен половой Надо так назвать - Vagee , Ingener (??), 01:16 , 10-Апр-21, (31) –1 Они там все шутники Например, язык Agda, цитата из вики Agda is named after the, Аноним (32), 01:18 , 10-Апр-21, (32) +1 А питон этих дам не отпугивает , Аноним (35), 01:20 , 10-Апр-21, (35) +2 // Многие его не любят, но многие пользуются - на жалость пробивает, вестимо , Аноним (50), 03:22 , 10-Апр-21, (50) К ч 235 рту Coq, дамы Лучше я познакомлю вас со своим Python-ом , Аноним (37), 01:29 , 10-Апр-21, (37) // твой питончик не идёт ни в какое сравнение с моей анакондой, Аноним (38), 01:49 , 10-Апр-21, (38) // Одноглазой, Аноним (117), 16:39 , 10-Апр-21, (117) Chick неплохой вариант , YetAnotherOnanym (ok), 02:07 , 10-Апр-21, (42) –1 Могут перейти на кириллицу и больше не будет проблем , Аноним (43), 02:23 , 10-Апр-21, (46) –2 Вечно эти женщины чем-то недовольны, Аноним (49), 03:00 , 10-Апр-21, (49) +2 // своей внутренней пустотой, видимо, Аноним (-), 06:55 , 10-Апр-21, (62) +1 // а ты заполняй чаще тогда тебе с утра не только пирожков напекут, но и ядро за т, Михрютка (ok), 18:11 , 10-Апр-21, (119) +2 // На редкость дельный совет , Annoynymous (ok), 12:17 , 11-Апр-21, (146) Зачем же так прочерчивать линию между мужчинами и женщинами На самом деле, боль, anonymous (??), 14:57 , 10-Апр-21, (108) Using the creator name s Coquand as Coq s full nameCoq would be viewed as an abb, Аноним (51), 03:31 , 10-Апр-21, (51) +1 Если an , n 1,2, - последовательность, то как политкорректно назвать an , anonimm (?), 03:58 , 10-Апр-21, (52) –1 Ну и что пусть меняют название, от этого мне не холоднее или теплее , Аноним (54), 04:07 , 10-Апр-21, (54) С 80-х годов существует и не было ни у кого проблем с названием А тут вдруг поя, nomad__ (ok), 06:54 , 10-Апр-21, (60) +1 // Ну а ещё не так давно в мире практиковалось рабство и это было традиционно норма, anonymous (??), 15:00 , 10-Апр-21, (109) // Нахрен этот идиотский мир , nomad__ (ok), 15:44 , 10-Апр-21, (112) до сих пор практикуется заключенные те же рабы и это нормально просто вы не зна, СеменСеменыч777 (?), 15:53 , 10-Апр-21, (113) // Цинизм - это нормально в отношении других Как и рабство А вот когда тебя - это, Аноним (82), 07:11 , 11-Апр-21, (130) если выражаться политкорректно философия и этика как её подраздел - это не ваша, СеменСеменыч777 (?), 08:50 , 11-Апр-21, (135) если неполиткорректно какой еще нашей культуре я отказываюсь иметь общую ку, СеменСеменыч777 (?), 08:58 , 11-Апр-21, (136) Да, место вздохов о слезинке ребёнка реально -- поводе для вторжения и гуманита, Michael Shigorin (ok), 21:18 , 11-Апр-21, (156) Только измельчали что-то, лампочки какие-то устаревшие, мелкошвейное производств, пох. (?), 16:28 , 11-Апр-21, (152) от хозяина зависит как известно, Виктор Бут мотает срок в США, там всех припахал, СеменСеменыч777 (?), 18:35 , 11-Апр-21, (153) +1 Тонкий передёрг Смешивание законов общества в одно время, с восприятием и тарак, Аноним (98), 23:04 , 10-Апр-21, (125) Почитайте про частные тюрьмы в штатах, много для себя узнаете нового насчёт был, Michael Shigorin (ok), 21:30 , 11-Апр-21, (158) Просто у этих женщин именно ОН и был на уме, к тому же слишком хорошее знание , Аноним (67), 07:31 , 10-Апр-21, (67) +2 coq это буквально петух с французского, где собственно находится инриа, занима, Аноним (72), 08:34 , 10-Апр-21, (72) +1 // Пойду скажу пацанам, что они в петухе PS Ты русский - освой Прям как не-родно, myhand (ok), 19:35 , 10-Апр-21, (121) У кого что болит , Аноним (74), 08:54 , 10-Апр-21, (75) –1 О доме надо думать , Аноним (76), 09:06 , 10-Апр-21, (76) Я знаю английский, и у меня не ассоциируется со сленговым Тут дело в характере , Аноним (-), 09:12 , 10-Апр-21, (77) +1 Ой, нашли проблему Переписать на питон, обозвать PyCoq - и членовраждующие сразу, тоже Аноним (ok), 11:42 , 10-Апр-21, (93) // PyCoq - а с чем тут будет ассоциация , Аноним (67), 11:57 , 10-Апр-21, (95) // Peacock, если хватит фантазии Если не хватит - ни с чем, что и требовалось , тоже Аноним (ok), 12:10 , 10-Апр-21, (96) +1 Осталось истеричкам-маразматичкам докопаться до FAQ - десятилетиями существоваше, Gogi (??), 11:43 , 10-Апр-21, (94) +2 // , не подсказывай , myhand (ok), 13:20 , 10-Апр-21, (101) +2 назло русским шовинистам переименовать в Habitually Used Inquiries, Михрютка (ok), 14:17 , 10-Апр-21, (106) +1 Давно пора одночлены и многочлены выкинуть из цисгендерной шовинистской мате, Аноним (99), 13:11 , 10-Апр-21, (99) Gallina лат курица Но это оскорбит российских феменисток , Аноним (117), 16:35 , 10-Апр-21, (114) // В СССР W России феминисток нет, Аноним (116), 16:37 , 10-Апр-21, (116) // Когда-то не было , Аноним (117), 16:41 , 10-Апр-21, (118) +1 // когда-то были А теперь если и есть, то лишь на спецзадании , Аноним (82), 07:14 , 11-Апр-21, (131) Ну тогда всем известный проект питон тоже нужно переименовать, Аноним (116), 16:36 , 10-Апр-21, (115) И сюда инклюзивные добралсь 129300 , rvs2016 (ok), 19:32 , 10-Апр-21, (120) // а ты я смарю не знаешь что значит это слово , Аноним (82), 07:15 , 11-Апр-21, (132) // Да опеннета ж начитаешься - и не такого узнаешь о , rvs2016 (ok), 10:43 , 11-Апр-21, (141) // На опеннете, кстати, уже родился как-то термин I инклюзиция I , Michael Shigorin (ok), 21:17 , 11-Апр-21, (155) +1 Я предпочёл бы не знать ни это слово, ни прочую xepотень, придуманную вами, альт, Аноним (164), 17:54 , 12-Апр-21, (165) Ну конечно галинабланка или кокос будет лучше К бабке не ходи , Аноним (173), 12:51 , 13-Апр-21, (173) 1,2,3,4,5,12,13,15,16,20,22,24,28,30,31,32,35,37,42,46,49,51,52,54,60,67,72,75,76,77,93,94,99,114,115,120,173

Сообщения

[Сортировка по времени | RSS]

	64. "Инструментарий для доказательства теорем Coq рассматривает в..."	+2 +/–
	Сообщение от Тот_Самый_Анонимус (?), 10-Апр-21, 06:59
	>но и формализацией математики занимаются на уровне, за которым уже целым институтам РАН не угнаться? Ради красного словца не пожалеем и отца? Разумеется подтверждения своим словм вы не приведёте.
	Ответить | Правка | Наверх | Cообщить модератору

	66. "Инструментарий для доказательства теорем Coq рассматривает в..."	+/–
	Сообщение от myhand (ok), 10-Апр-21, 07:06
	Ну, представленного общественности инструмента уровня Coq разработано было не было.  Не говоря уже о получении к-л известных формальных доказательств с ним...
	Ответить | Правка | Наверх | Cообщить модератору

Архив | Удалить

Рекомендовать для помещения в FAQ | Индекс форумов | Темы | Пред. тема | След. тема