@l29ah в idris

@l29ah да, там вся целочисленная арифметика на church numerals

@ninesigns и сами числа тоже

@anonymous насчёт охуенности не знаю, но тот факт что тип натуральных чисел строится на основе индукции от Z, никак не связан невозможностью выражения чисел и арифметических операций с ними в нативных типах платформы.

@anonymous ну блядь пиздец, 2017 год блять, а вот что делать с оверфлоу не знаем.

@anonymous я думаю, компилятор вправе сунуть нативный тип для которого есть доказательство что он не превысит лимиты значений