3 search results for "tag:"logpath:HOLLight""

Showing 1 - 3

coq-hol-light

No documentation

HOL-Light library in Coq

logpath:HOLLight date:2025-01-20 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers category:Mathematics/Real Calculus and Topology keyword:HOL-Light keyword:list keyword:basic set theory keyword:arithmetic keyword:integer keyword:real keyword:complex keyword:permutation keyword:group keyword:matroid keyword:binomial keyword:topology keyword:metric keyword:space keyword:analysis keyword:homology keyword:vector keyword:linear keyword:algebra keyword:convex keyword:path keyword:polytope keyword:Brouwer keyword:degree keyword:derivative keyword:Clifford keyword:integration keyword:measure keyword:Lebesgue keyword:transcendental

Frédéric Blanqui

3.0.0

CeCILL-2.1

Used by 0 other packages

21 Jan 2025
coq-hol-light-real-with-N

No documentation

Definition of HOL-Light real numbers in Coq using N

logpath:HOLLight_Real_With_N date:2025-07-11 category:Mathematics/Arithmetic and Number Theory/Miscellaneous category:Mathematics/Real Numbers keyword:HOL-Light

https://github.com/Deducteam/coq-hol-light-real-with-N/blob/main/AUTHORS.md

2.0.0

CeCILL-2.1

Used by 1 other packages

11 Jul 2025
coq-hol-light-real-with-nat

No documentation

Definition of HOL-Light real numbers in Coq using nat

keyword:HOL-Light category:Math/Arith/Misc category:Math/Arith/Real numbers date:2024-11-03 logpath:HOLLight_Real

Frédéric Blanqui

1.0.0

CeCILL-2.1

Used by 1 other packages

20 Jan 2025