Skip to content

Latest commit

 

History

History
12 lines (9 loc) · 438 Bytes

File metadata and controls

12 lines (9 loc) · 438 Bytes

Base Conversion of Integers

We propose here an encoding of natural numbers in base 10 (or 16) for easy parsing and printing. Then we provide conversion functions between these base-10 and base-16 numbers and Coq usual numerical datatypes (nat, N, positive, Z, ...) and we prove the correctness of these conversion functions.

Initial Author : Pierre Letouzey, April 2016

License : LGPL (see the LICENSE file)