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 specyfying a data structure, where
- Checking for overflows of the length is hard (and may leak to the users of the library)
- Overflows are impossible, because objects are always created one-by-one.
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.