Hello, looking into the anaylsis library as I was recommended. Currently, I am having hard time browsing around which file does what. Is there an index file, or a way to generate some kind of index file to view certain definition?

Anything more convenient than aimlessly browsing on the github repo would be nice!

By the way, is there a function space of a everywhere-differentiable function defined? Or C^1 and C^\infty spaces?

see research papers: https://math-comp.github.io/papers.html

And maybe more specifically the "related publications" listed here https://github.com/math-comp/analysis/#meta

We have generated the following "documentation" using coqdoc, it may help you browse the code: https://math-comp.github.io/analysis/htmldoc_0_5_3/

Thank you all!

abab9579 has marked this topic as resolved.

Last updated: Dec 07 2023 at 17:01 UTC