GitHub topics: hol2dk
Deducteam/coq-hol-light-real-with-N
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
Language: Rocq Prover - Size: 110 KB - Last synced at: 5 days ago - Pushed at: 12 days ago - Stars: 2 - Forks: 5
Deducteam/coq-hol-light-real-with-nat
Translation in Rocq of the HOL-Light definition of real numbers using the Rocq type nat
Language: Rocq Prover - Size: 238 KB - Last synced at: 6 days ago - Pushed at: 12 days ago - Stars: 3 - Forks: 2
Deducteam/coq-hol-light-Logic1
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
Language: Rocq Prover - Size: 744 KB - Last synced at: 7 days ago - Pushed at: 22 days ago - Stars: 0 - Forks: 1