Module nat_int 

Bignum dispatch — externs from lean.h:1334–1853 plus the small-int ceiling constants.

Constants

LEAN_MAX_SMALL_INT

Largest scalar-encodable Int (lean.h:1544). On 64-bit hosts this is i32::MAX; on 32-bit hosts it is i32::MAX >> 1.

LEAN_MAX_SMALL_NAT

Largest Nat that fits in a scalar pointer (lean.h:1336). On 64-bit hosts this is usize::MAX >> 1.

LEAN_MIN_SMALL_INT

Smallest scalar-encodable Int (lean.h:1545).

Functions

lean_big_int64_to_int^⚠

lean_big_int_to_int^⚠

lean_big_size_t_to_int^⚠

lean_big_uint64_to_nat^⚠

lean_big_usize_to_nat^⚠

lean_cstr_to_int^⚠

lean_cstr_to_nat^⚠

lean_int_big_add^⚠

lean_int_big_div^⚠

lean_int_big_div_exact^⚠

lean_int_big_ediv^⚠

lean_int_big_emod^⚠

lean_int_big_eq^⚠

lean_int_big_le^⚠

lean_int_big_lt^⚠

lean_int_big_mod^⚠

lean_int_big_mul^⚠

lean_int_big_neg^⚠

lean_int_big_nonneg^⚠

lean_int_big_sub^⚠

lean_nat_big_add^⚠

lean_nat_big_div^⚠

lean_nat_big_div_exact^⚠

lean_nat_big_eq^⚠

lean_nat_big_le^⚠

lean_nat_big_lt^⚠

lean_nat_big_mod^⚠

lean_nat_big_mul^⚠

lean_nat_big_sub^⚠

lean_nat_big_succ^⚠

lean_nat_overflow_mul^⚠

lean_uint8_of_big_nat^⚠