package rocq-hollight
HOL-Light library in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
1.1.0.tar.gz
sha256=eddac4a3dc5a728125a04861582e704f16c4b216f503f3b9f78e5521d2fc4d57
sha512=47af30ec5645bd140be5297deb02d4b7af72758596d3f50ee13c6f52c98379ee2b762820cbc462a0a1553eafc403334ff9d6b0cfd12409ff56a5acb3629b26f5
Description
This library contains an automatic translation in Rocq of the HOL-Light library using hol2dk and lambdapi.
Tags
logpath:HOLLight date:2026-09-18 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendentalPublished: 19 Sep 2026
Dependencies (5)
-
rocq-equations
>= "1.3.1+9.0" - rocq-mathcomp-zify
-
coq-fourcolor-reals
>= "1.4.2" -
rocq-mathcomp-algebra
>= "2.6" - rocq-mathcomp-analysis-stdlib
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page