CoRN

github.comtool

Library of constructive real analysis and algebra.

from

Coq

added

2026-10-10

likes

0

similar

1. ▲
   CoLoR github.com

   tool category #coq link ↗

   Library on rewriting theory, lambda-calculus and termination, with sub-libraries on common data structures extending the Coq standard library.

   
2. ▲
   Analysis github.com

   tool category #coq link ↗

   Library for classical real analysis compatible with Mathematical Components.

3. ▲
   ExtLib github.com

   tool category #coq link ↗

   Collection of theories and plugins that may be useful in other Coq developments.

   
4. ▲
   Coq-Kruskal github.com

   tool category #coq link ↗

   Collection of libraries related to rose trees and Kruskal's tree theorem.

   
5. ▲
   Coqtail Math github.com

   tool category #coq link ↗

   Library of mathematical results ranging from arithmetic to real and complex analysis.

   
6. ▲
   TLC github.com

   tool category #coq link ↗

   Non-constructive alternative to Coq's standard library.

   

Coq › Projects > Type Theory and Mathematics: “Library of constructive real analysis and algebra.”