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