ᛒ
Size: a a a
2020 June 10
Oℕ
Oℕ
мало того, что аллоцируют
Oℕ
так ещё и сериализуют это говно
AG
сделать что ли две системы
AG
минимальную и с инверсором
AG
еще с рекурсором можно
AG
а впрочем хер с ним
AG
лучше коиндуктивные сделаю
Oℕ
шо такое инверсор
AG
шо такое инверсор
ну тип распаковать один слой мю
AG
In : Term g (subst1T f (Mu f)) -> Term g (Mu f)
Ni : {f : Ty (S n)} -> Term g (Mu f) -> Term g (subst1T f (Mu f))
Oℕ
Understandable
в котах кстати и делают чтобы instances был не нужен, мистер Коричневый в марте смержил ещё
в котах кстати и делают чтобы instances был не нужен, мистер Коричневый в марте смержил ещё
покажи
AG
точнее наоборот запаковать
w
точнее наоборот запаковать
Эх, сча бы запаковать
SK
Самый красивый.
Анонимный опрос
7%
Бразильяновск.
67%
Чичня.
27%
Шымкент.
Oℕ
ну тип распаковать один слой мю
понятно
AG
понятно
с ним получается
pred : Term g (NAT ~> Sum U NAT)
pred = Lam $ Ni $ Var Here