Expand description
Arbitrary-precision integer for the Aver runtime.
Aver’s Int is mathematical ℤ: total, never wrapping, faithful to the
Lean/Dafny proof model. AverInt is the runtime carrier for that model.
It is small-int optimized: any value that fits an i64 is stored inline
as Small, and only genuinely large magnitudes spill to a heap BigInt.
Native machine-integer speed is a separate, opt-in concern (a bounded
refinement type whose carrier the compiler lowers to raw i64); it is not
this type’s job. AverInt is correctness-first: every arithmetic operation
produces the exact mathematical result.
§Canonical form
The single invariant every constructor and operation upholds: a value that
fits i64 is always Small. A Big payload never holds a value in
[i64::MIN, i64::MAX]. This makes the representation canonical, so derived
Eq, Ord, and Hash are unique — two numerically-equal values always
compare and hash identically regardless of how they were built. Map/Set
keying depends on this.
Enums§
- AverInt
- Arbitrary-precision integer (mathematical ℤ) with a small-int fast path.