Телеграмм чат группы haskell

кана

ну все "такие" списки

Ну да

17:33пожаловаться #1

https://t.me/haskell_blah/260121

Alex Gryzlov in haskell_blah

ну вот очевидное следствие: https://github.com/gallais/potpourri/blob/master/agda/cubical/list0.agda#L14

Капец, вам нормально в Юникод писать? Это же гемор

17:34пожаловаться #2

Почему вы ето делаете

17:34пожаловаться #3

мне нет, я агдой не пользуюсь

17:34пожаловаться #4

кана in haskell_blah

поставиь lean плагин в vscode

17:34пожаловаться #5

кана in haskell_blah

там оч удобно писать юникод

17:34пожаловаться #6

и лином тож

17:34пожаловаться #7

а в коке и идрисе не особо принят юникод

17:34пожаловаться #8

а в коке и идрисе не особо принят юникод

И это прекрасно)

17:35пожаловаться #9

https://t.me/haskell_blah/260121

Alex Gryzlov in haskell_blah

ну вот очевидное следствие: https://github.com/gallais/potpourri/blob/master/agda/cubical/list0.agda#L14

Чето ваще неясно

17:36пожаловаться #10

Ну то есть по-русски если -- то ясно

17:36пожаловаться #11

А так -- неясно

17:36пожаловаться #12

ну кубы они не очень интуитивные да

Screen Recording 2020-12-04 at 17.36.42.mp4

17:36пожаловаться #13

кана in haskell_blah

(372.61 Кб)

17:37пожаловаться #14

там желательно уже иметь некоторый опыт с интенсиональными завтипами и зависимым патматом

17:37пожаловаться #15

Screen Recording 2020-12-04 at 17.36.42.mp4

кана

(372.61 Кб)

Понятно теперь, как вы енто делаете. Теперь и в агду вкатываться можно

17:38пожаловаться #16

Screen Recording 2020-12-04 at 17.36.42.mp4

кана

(372.61 Кб)

я для подобного использую просто https://marketplace.visualstudio.com/items?itemName=yellpika.latex-input если надо

Visualstudio

latex-input - Visual Studio Marketplace

Extension for Visual Studio Code - LaTeX-style unicode input

17:38пожаловаться #17

Roman in haskell_blah

Представил как хорошо было бы писать в юникоде, если каждый символ нужно было бы вбивать alt кодами.

17:38пожаловаться #18

плагин правда походу сгнил, надо поискать посвежее аналог

17:39пожаловаться #19

плагин правда походу сгнил, надо поискать посвежее аналог

Так Кана же кинул)