HOL-Light to Dedukti/Lambdapi translator
-
Updated
Dec 15, 2025 - Rocq Prover
#
hol-light
Here are 9 public repositories matching this topic...
Translation of HOL-Light's Multivariate library in Rocq
-
Updated
Nov 19, 2025 - Rocq Prover
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
-
Updated
Nov 24, 2025 - Rocq Prover
HOL-Light Library for Modal Systems
theorem-proving proof-assistant higher-order-logic interactive-theorem-proving modal-logics automated-theorem-proving hol-light
-
Updated
Aug 23, 2025 - OCaml
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
-
Updated
Dec 2, 2025 - Rocq Prover
Translation of HOL-Light's Logic library in Rocq
-
Updated
Dec 3, 2025 - Rocq Prover
HOL Light Library for Modal Systems
theorem-proving proof-assistant higher-order-logic modal-logic interactive-theorem-proving automated-theorem-proving hol-light
-
Updated
Nov 27, 2025
Translation in Rocq of the HOL-Light definition of real numbers using MathComp
-
Updated
Nov 25, 2025 - Rocq Prover
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
-
Updated
Dec 15, 2025 - Rocq Prover
Improve this page
Add a description, image, and links to the hol-light topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the hol-light topic, visit your repo's landing page and select "manage topics."