M
Я вот за простоту логики
Size: a a a
2020 July 09
AG
где первый аргумент бокса - свободные переменные внутри макроса
C
Это ещё более логично
Нельзя так делать, Алекс рил пытается тебе что-то объяснить.
C
идея примерно такая, что если у нас есть макрос производящий программу типа B, и есть макрос, производящий макрос, производящий программу типа С, то мы можем сделать макрос, производящий программу С напрямую
Ты забыл указать связь между В и С
AG
да просто много букв получилось бы
C
да просто много букв получилось бы
Иначе не имеет смысла такое описание. Удали.
AG
Иначе не имеет смысла такое описание. Удали.
докажи вот лучше
map2 : Term d g (Box [a] (a ~> b) ~> Box [b] c ~> Box [a] c)M
Нельзя так делать, Алекс рил пытается тебе что-то объяснить.
Насколько я поняла, задача состоит в том, чтобы уменьшить количество условных операций до программы C
AG
Насколько я поняла, задача состоит в том, чтобы уменьшить количество условных операций до программы C
ну тип врезать один макрос в другой
AG
смысл в том что доказательства в интуиционистской контекстуальной модальной логике это метапрограммы, умеющие манипулировать квазицитатами произвольного уровня вложенности
AG
плюс свободными переменными
C
Насколько я поняла, задача состоит в том, чтобы уменьшить количество условных операций до программы C
...
M
смысл в том что доказательства в интуиционистской контекстуальной модальной логике это метапрограммы, умеющие манипулировать квазицитатами произвольного уровня вложенности
Понимаю
C
Что?
Где ответ на задачу?
M
Где ответ на задачу?
Извини, я ещё не смотрела. Я работала с момента пробуждения практически, времени не было.
M
Да, вообще-то
M
Я временами только на конфу отвлекалась
M
И ныла, что сложно выйти за сигаретами