Expand description
Peano integers
Peano integers are a specialized kind of integers, that allow to increase the integer without checking for overflows.
See https://inria.hal.science/hal-01162661v1 for reference.
§Usage in data structures
They are useful when specifying a data structure where
- checking for overflows of the length is hard (and may leak to the users of the library),
- overflows are practically impossible because the length only grows by one at a time.
In this case, you could use a PeanoInt to store the length.
§Why not always use them ?
Well, simply because you cannot add two peano integers together, at least not efficiently. If you need to do usual arithmetic operations, you should use a normal integer.
§Ghost code
You cannot increase a peano integer in ghost code, as it may
overflow the backing integer. Since ghost code is not executed, the time argument is
not applicable.
Structs§
- Peano
Int - A peano integer wrapping a 64-bits integer.