История изменений
Исправление quasimoto, (текущая версия) :
где это «где-то там»?
Конкретно я написал на Agda2. Ну и в других подобных языках есть такой тип в удобном (в математическом смысле) виде.
вот именно
Ну вот. А желателям помучить сишку можно посмотреть на книжку EoP и в сторону верификаторов для сишки (там и фиксед поинт и флоат будет).
Только это тоже не кольцо, и тем более не поле. Потому все свои аксиомы можешь отложить в сторону.
Что с ними делать в рамках твоей теории чисел основанной на аксиомах Пеано — я не понимаю.
Так ты не перекладывай с одного на другое — есть N, Z/nZ, {4, 6, ..., 40}, три разных типа, три разных набора аксиом и разные свойства. Была продемонстрирована эквивалентность двух функций на N, любые другие подобные эквивалентности и свойства на других типах доказываются аналогично.
Исходная версия quasimoto, :
где это «где-то там»?
Конкретно я написал на Agda2. Ну и в других подобных языках есть такой тип в удобном (в математическом смысле) виде.
вот именно
Ну вот. А желателям помучить сишку можно посмотреть на книжку EoP и в сторону верификаторов для сишки (там и фиксед поинт и флоат будет).
Только это тоже не кольцо, и тем более не поле. Потому все свои аксиомы можешь отложить в сторону.
Что с ними делать в рамках твоей теории чисел основанной на аксиомах Пеано — я не понимаю.
Так ты не перекладывай с одного на другого — есть N, Z/nZ, {4, 6, ..., 40}, три разных типа, три разных набора аксиом и разные свойства. Была продемонстрирована эквивалентность двух функций на N, любые другие подобные эквивалентности и свойства на других типах доказываются аналогично.