Translation of HOL-Light's Multivariate library in Rocq
-
Updated
Jan 1, 2026 - Rocq Prover
#
hol2dk
Here are 6 public repositories matching this topic...
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
-
Updated
Nov 24, 2025 - Rocq Prover
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
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 hol2dk topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the hol2dk topic, visit your repo's landing page and select "manage topics."