к
Я так и написал(
а да
Size: a a a
2020 December 04
к
тогда все верно
к
между точками 0 и 1 в натуральных числах очевидно нет непрерывного пути
DB
между точками 0 и 1 в натуральных числах очевидно нет непрерывного пути
Так точно
к
потому что между 0 и 1 вообще нет других точек
к
в натуральных числах
AG
но можно его задать аксиоматически :)
к
но если задать его аксиоматически, то будет, да
к
точно так же как мы задаем аксимоматически что есть пространство Nat, и в нем есть точка 0 и другие точки из других точек
DB
но можно его задать аксиоматически :)
А ничего не сломается, если так сделать?
AG
все сломается
AG
будет аналог нулевых списков выше
AG
сколько ни добавляй, всё 0
к
data Nat0 where
0 : Nat0
S : Nat0 -> Nat0
P : 0 = S 0
0 : Nat0
S : Nat0 -> Nat0
P : 0 = S 0
к
вот этот P это аксиома что между 0 и 1 есть путь
к
так индуктивно получается что существуют пути между всеми точками в 0
к
значит по сути Nat0 это тип с одним значением 0
к
а все остальные значения доказуемо равны нулю
к
поэтому ничего не сломается, ведь при паттерн-матчинге этого Nat0 нам нужно обрабатывать не только 0 и Succ, но и P
AG
это просто слишком убойные ограничения