HOL-Light definition of real numbers in Rocq using N and MathComp
Install
Dune Dependency
Authors
Maintainers
Sources
0.0.0.tar.gz
sha256=e31c68256ee15b2d154217aeea83ff8dfa29a30d6d11073f8807d5cd993b82d0
Description
This library contains an automatic translation in Rocq of the HOL-Light definition of real numbers using https://github.com/Deducteam/hol2dk.
Tags
logpath:MathComp_HOLLight_Real_With_N date:2025-07-11 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers keyword:HOL-LightPublished: 02 Oct 2025
Dependencies (2)
-
rocq-prover
>= "9.0" -
coq-mathcomp-classical
>= "1.8.0"
Dev Dependencies
None
Used by (2)
Conflicts
None
On This Page