blob: 4c217f3fb09f4720f950d7cad3841bab6205f10b (
plain)
1
2
3
4
5
6
|
- **Added:**
``Cantor.v`` containing the Cantor pairing function and its inverse.
``Cantor.to_nat : nat * nat -> nat`` and ``Cantor.of_nat : nat -> nat * nat``
are the respective bijections between ``nat * nat`` and ``nat``.
(`#14008 <https://github.com/coq/coq/pull/14008>`_,
by Andrej Dudenhefner).
|
