abab9579 (Aug 18 2022 at 07:00): abab9579 (Aug 18 2022 at 07:00):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?
Karl Palmskog (Aug 18 2022 at 08:28):see research papers: https://math-comp.github.io/papers.html
Pierre Roux (Aug 18 2022 at 10:00):And maybe more specifically the "related publications" listed here https://github.com/math-comp/analysis/#meta
Reynald Affeldt (Aug 18 2022 at 10:07):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/
abab9579 (Aug 18 2022 at 11:33):Thank you all!
Notification Bot (Aug 20 2022 at 02:03):abab9579 has marked this topic as resolved.
Last updated: Dec 07 2023 at 17:01 UTC