Stream: math-comp analysis

Topic: Where to access documentation


view this post on Zulip 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?

view this post on Zulip Karl Palmskog (Aug 18 2022 at 08:28):

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

view this post on Zulip Pierre Roux (Aug 18 2022 at 10:00):

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

view this post on Zulip 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/

view this post on Zulip abab9579 (Aug 18 2022 at 11:33):

Thank you all!


Last updated: Jan 30 2023 at 11:03 UTC