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 the Multivariate library of HOL-Light. It contains more than 20,000 theorems on arithmetic, wellfounded relations, lists, real numbers, integers, basic set theory, permutations, group theory, matroids, metric spaces, homology, vectors, determinants, topology, convex sets and functions, paths, polytopes, Brouwer degree, derivatives, Clifford algebra, integration, measure theory, complex numbers and analysis, transcendental numbers, real analysis, complex line integrals, etc.
Tags
logpath:HOLLight date:2025-01-20 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: 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