AD
Но ведь в том же Coq доказательство проверяется при "компиляции".
Если есть T(n) forall n:nat, Word n, можно получить в любом месте програмы T(m) и иметь там Word m
Size: a a a
2020 July 24
AD
Даже после компиляции
IZ
А std::variant<float, vector<int>> можешь?)
Я всё могу...
RR
Я всё могу...
Кроме корректных доказательств?)
AM
Как вариант: https://github.com/kaltura/nginx-vod-module + любой hls плеер (videojs, clappr и т.д.)
Ок. спасибо. посмотрю
PB
Ребят, есть такой "фреймворк" -
OpenCASCADE, коллега пишет библиотечку, использующую его функционал. Так же, добрыми людьми была написана обвязка OpenCASCADE для Python (с помощью SWIG), которая называется pythonocc. Необходимо дёргать функции нашей библиотеки из Python, да ещё и таким образом, что бы возвращаемые объекты были объектами pythonocc. Вопрос, как такое сделать?m
Вот поэтому я был против юникода в именах переменных.
TS
да, это путь в ад. а сколько там невидимых символов сейчас? может просто их приравнять whitespace в лексере?
AZ
не в ад, а в современную разработку
AD
да, это путь в ад. а сколько там невидимых символов сейчас? может просто их приравнять whitespace в лексере?
Если всё оттайплено, то вайнот? Выразительный синтаксис всегда хорошо
NP
Ребят, есть такой "фреймворк" -
OpenCASCADE, коллега пишет библиотечку, использующую его функционал. Так же, добрыми людьми была написана обвязка OpenCASCADE для Python (с помощью SWIG), которая называется pythonocc. Необходимо дёргать функции нашей библиотеки из Python, да ещё и таким образом, что бы возвращаемые объекты были объектами pythonocc. Вопрос, как такое сделать?кажется, это скорее вопрос про питон, а не про плюсы: о том, как дергать нативный код из питона
NP
а как это работает? не могу понять как срабатывает перегрузка если у нас нет инстанса
magic_absm
да, это путь в ад. а сколько там невидимых символов сейчас? может просто их приравнять whitespace в лексере?
Не знаю имеет ли смысл. Это же всего лишь одна из проблем юникода и кажется не самая страшная. Переменные на русском намного страшнее. И там есть ошибки вида
сommad где c - это русская C. И такие ошибки могут возникнуть в реальном коде.AD
Не знаю имеет ли смысл. Это же всего лишь одна из проблем юникода и кажется не самая страшная. Переменные на русском намного страшнее. И там есть ошибки вида
сommad где c - это русская C. И такие ошибки могут возникнуть в реальном коде.Линтеры же?
m
Линтеры же?
И чем поможет линтер?
DF
Русский язык забанит
AD
И чем поможет линтер?
бан переменных на руском или миксланг идентификаторов
AD
хотя я лично юзал нелатинские символы для формулок, потому что они иначе превращались в огромную кашу и с пейпером сравнивать было проблематично.