package coq-hol-light
HOL-Light library in Coq
Install
Dune Dependency
Authors
Maintainers
Sources
3.0.0.tar.gz
sha256=69d18497628469a8fbb1e120c158f25c81e32cef70edf5f28f3b4ac9f488602f
Description
This library contains an automatic translation in Coq of (for the moment) some small part the HOL-Light library using https://github.com/Deducteam/hol2dk.
Tags
logpath:HOLLight date:2025-01-20 category:Math/Arith/Misc category:Math/Arith/Real Numbers category:Math/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: 21 Jan 2025
Dependencies (3)
-
coq-fourcolor-reals
>= "1.4.0" -
coq-hol-light-real-with-N
>= "1.0" -
coq
>= "8.19"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page