forum.opennet.ru

"Инструментарий для доказательства теорем Coq рассматривает возможность смены названия"

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

Исходное сообщение

[ Отслеживать ]

. "Инструментарий для доказательства теорем Coq рассматривает в..."	+3 +/–
Сообщение от Аноним (20), 10-Апр-21, 00:02
Но вообще правильно, слишком грубо это. Наверняка все шутят постоянно. >The name Coq comes from the French word for rooster, CoC (the Calculus of Constructions) and Thierry Coquand, one of the initial authors of Coq Предлагаю что-нибудь более нейтральное, например, Diq - Development of Information Constuctions (по мотивам оригинала). Подойдёт?
Ответить \| Правка \| Наверх \| Cообщить модератору

Оглавление

Инструментарий для доказательства теорем Coq рассматривает возможность смены названия, opennews, 09-Апр-21, 23:22 [смотреть все]

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

Форумы | Темы | Пред. тема | След. тема

Партнёры:

Хостинг:

Закладки на сайте
Проследить за страницей

Created 1996-2024 by Maxim Chirkov
Добавить, Поддержать, Вебмастеру