package rocq-hollight
HOL-Light library in Rocq
Install
Dune Dependency
Authors
Maintainers
Sources
1.0.0.tar.gz
sha256=04ac9b715d21940f911e0c3d5632ff63ebec82f019050992969cf062fc40cef2
sha512=67ff0a86a9f65d8a786ac7f18577f7abb09e00b0326d1b678f2235e872df0250652bccb49d3348807e9df03152de9bf2ae18505674203bdc8582fefcc19e1204
Description
This library contains an automatic translation in Rocq of the HOL-Light library using hol2dk and lambdapi.
Tags
logpath:HOLLight date:2026-09-08 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: 09 Sep 2026
Dependencies (7)
-
rocq-equations
>= "1.3.1+9.0" -
coq-mathcomp-zify
>= "1.6.0" -
coq-fourcolor-reals
>= "1.4.2" -
coq-mathcomp-algebra
< "2.6.0" -
coq-mathcomp-analysis-stdlib
>= "1.14.0" -
coq-mathcomp-classical
>= "1.16.0" -
rocq-prover
>= "9.0"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page