R
Size: a a a
2021 March 13
E
ух ебать же идрис силен
E
только сигнатурки расставить, круды сами пишутся
E
истинный премиум
AG
внезапные расширения Кана
AG
чот вспомнилось как мы попросили спивака на пальцах их объяснить
AG
написали ему на доске
record Ran (j : Type -> Type) (g : Type -> Type) (x : Type) и он припухAG
а чё это у вас грит одна категория на всё про всё что ли
E
я пока не дошел до синтаксиса
{ 0 b : Nat -> Type } и дата структуры уже решил вдень почитатьAG
это стираемый имплицит
E
а чё это у вас грит одна категория на всё про всё что ли
я кстати вопросом задавался
AG
параметр который существует только при компиляции и выводится сам
AG
то есть это по сути такая внутренняя деталь, проводка в стене
E
а можно как-то ограничить этот скоуп типов?