package coq-hol-light-real-with-N
Definition of HOL-Light real numbers in Coq using N
Install
Dune Dependency
Authors
Maintainers
Sources
1.2.0.tar.gz
sha256=bfd5a1cd356b2208d4989d7024c694bf984816e85b479e8ec12319e75ab0c9bf
Description
This library provides a representation in Coq of the definition of real numbers in HOL-Light, using the Coq type N for natural numbers, automatically generated from HOL-Light using hol2dk and lambdapi.
Tags
logpath:HOLLight_Real_With_N date:2025-02-19 category:Math/Arith/Misc category:Math/Arith/Real numbers keyword:HOL-LightPublished: 13 Mar 2025
Dependencies (1)
-
coq
>= "8.19"
Dev Dependencies
None
Used by (1)
-
coq-hol-light
>= "3.0.0"
Conflicts
None
On This Page