GitHub topics: rocq-prover
Deducteam/rocq-hollight-logic-unif
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
Language: Rocq Prover - Size: 596 KB - Last synced at: about 11 hours ago - Pushed at: about 17 hours ago - Stars: 0 - Forks: 2
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: 114 KB - Last synced at: 3 days ago - Pushed at: 21 days ago - Stars: 2 - Forks: 5
Deducteam/hol2dk
HOL-Light to Dedukti/Lambdapi translator
Language: Rocq Prover - Size: 719 KB - Last synced at: 3 days ago - Pushed at: 21 days ago - Stars: 8 - Forks: 6
Deducteam/coq-hol-light
HOL-Light library in Coq
Language: Rocq Prover - Size: 1.28 MB - Last synced at: 3 days ago - Pushed at: about 2 months ago - Stars: 7 - Forks: 3
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: 241 KB - Last synced at: 4 days ago - Pushed at: 2 months ago - Stars: 3 - Forks: 2