Skip to content

letouzey/baseconv

Repository files navigation

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)

About

Base Conversion of Integers (from base 10 or 16 to Coq usual datatypes)

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published