package rocq-hollight-logic-unif
HOL-Light library necessary for translating unify
Install
Dune Dependency
Authors
Maintainers
Sources
0.0.0.tar.gz
sha256=3f09cb1836850027bdf5c7e681e299c3c6675e083f99ce846e09b2b72f714cde
sha512=6567b620d058fe09ce373c2cbcb2e0a08c3f0ecfedf348967dfe3f64568ea6750c298add17901831c94ec39dea5aa93d8d0c62549651744b86e0890a168b7cd5
Description
This library contains an automatic translation in Rocq of a part of the HOL-Light Logic library using https://github.com/Deducteam/hol2dk.
Tags
logpath:HOLLight_Logic_fole date:2025-10-16 keyword:HOL-Light keyword:first order logicPublished: 22 Oct 2025
Dependencies (5)
-
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 (1)
Conflicts
None
On This Page