Sujet: "hol-light"
Deducteam/hol2dk
HOL-Light to Dedukti/Lambdapi translator
langage: Rocq Prover - taille: 690 ko - dernière synchronisation: il y a 4 jours - enregistré: il y a 6 jours - étoiles: 7 - forks: 6
Deducteam/coq-hol-light
Translation of HOL-Light's Multivariate library in Rocq
langage: Rocq Prover - taille: 1,28 Mo - dernière synchronisation: il y a 4 jours - enregistré: il y a 18 jours - étoiles: 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
langage: Rocq Prover - taille: 243 ko - dernière synchronisation: il y a 5 jours - enregistré: il y a 13 jours - étoiles: 3 - forks: 2
Deducteam/coq-hol-light-real-with-N
Translation in Coq of the HOL-Light definition of real numbers using binary natural numbers
langage: Rocq Prover - taille: 160 ko - dernière synchronisation: il y a 4 jours - enregistré: il y a 5 jours - étoiles: 2 - forks: 5
Deducteam/rocq-hollight-logic
Translation of HOL-Light's Logic library in Rocq
langage: Rocq Prover - taille: 748 ko - dernière synchronisation: il y a 2 jours - enregistré: il y a 4 jours - étoiles: 1 - forks: 2
Deducteam/rocq-hollight-logic-unif
Translation in Rocq of HOL-Light's Logic library until unify using hol2dk
langage: Rocq Prover - taille: 600 ko - dernière synchronisation: il y a 2 jours - enregistré: il y a 4 jours - étoiles: 0 - forks: 2
Deducteam/mathcomp-hollight-real-with-N
Translation in Rocq of the HOL-Light definition of real numbers using MathComp
langage: Rocq Prover - taille: 104 ko - dernière synchronisation: il y a environ 21 heures - enregistré: il y a 12 jours - étoiles: 0 - forks: 2