AG
@clayrat я прально сказал ему, сенсей?
та да
Size: a a a
2020 June 04
A
та да
хзмхзмхзхзхмз
Oℕ
/set /set /get
да ви знаток секвенций
AG
ну в целом говорить что индексы всегда стираются это конечно сильное упрощение
AG
вокруг этого целую науку развели, с пропами, нулевыми модальностями, иррелевантностью и прочим хоттом
ᛒ
вокруг этого целую науку развели, с пропами, нулевыми модальностями, иррелевантностью и прочим хоттом
AG
но базовая идея индексов это просто доп информация в типе, начиная с конкретных типов вместо переменных в гадтах, и заканчивая термами в завтипах
R
когда будем проходить
R
но базовая идея индексов это просто доп информация в типе, начиная с конкретных типов вместо переменных в гадтах, и заканчивая термами в завтипах
ты не мог бы ввести этот термин для тупых в ковелью?
w
ты не мог бы ввести этот термин для тупых в ковелью?
Пешка Кодзимы!
R
с примерами
ᛒ
когда будем проходить
скажи мне раттенк
R
можно попозже летом, когда каникулы в вузе будут
AG
да просто посмотри на гадты еще раз
R
то что мой член суммы фиксирует конкретный тип в адт это уже индекс да?
AG
ну я не уверен в терминологии но по сути да
R
это трансляция из кода
AG
обычно все же индексом называют терм, вшитый в индуктивное семейство, но суть примерно та же