[
В Haskell просто нет Nat
А нормальные числа и в Idris не выражены через Пеано, это ж безумно плохо по производительности
Size: a a a
2021 May 31
[
Там и нат приводят в интегеры
[
Не совсем
[
enum Fin<N>{
Z,
S(Fin<N-1>),
}
gо
Да, действительно
SS
[
Считаю, что рекурсивные определения это идиоматично
[
Там кстати сигнатура неправильная у gen на скрине, надо n + 1 + m возвращать
[
Где m это любой Nat
r
Точнее завтипы позволяют написать доказательство того, что программа/функция делает то-то и то-то (в частности, не крашится).
gо
Можно просто разрешить конвертировать Fin n в Fin m где n < m
[
Можно
[
Я по сути это и делаю
[
А, кстати, хуйня
а
Что такое Fin
[
Там всё определение
а
Не, какой смысл вложен в слово Fin
а
типа Final или чего
AN
А как выражены? Как грёбаный Nat выражен в рантайме? И это только Nat или любое похожее рекурсивное определение можно свернуть так?