package rocq-hollight-logic
HOL-Light library necessary for translating unify
Install
Dune Dependency
Authors
Maintainers
Sources
0.0.0.tar.gz
sha256=7a51d9a9df0d42ed997a2c5169d2d0c240b6bfcd980d865fe6849c8a7113e8a0
sha512=2d865b655172e21c0f74e8c75441ccfe15eef744e6bc6bfbf3988c748929ceaa3ab27f0f4edcce104c929e4a2602afdf01651237748d1b18d51ca01a239ccf88
Description
This library contains an automatic translation in Rocq of the HOL-Light Logic library using https://github.com/Deducteam/hol2dk.
Tags
logpath:HOLLight_Logic date:2025-10-21 keyword:HOL-Light keyword:first order logicPublished: 25 Oct 2025
Dependencies (6)
-
rocq-hollight-logic-unif
>= "0.0.0" -
rocq-equations
>= "1.3.1+9.0" -
rocq-mathcomp-hollight-real-with-N
>= "0.0.0" -
coq-fourcolor-reals
>= "1.4.0" -
coq-mathcomp-classical
>= "1.8.0" -
rocq-prover
>= "9.0"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page