Yannick Forster
Yannick Forster
When @dominik-kirst was hunting the universe problem, I tried to create a dependency graph of the library, but without success. With the help of the Enrico Tassi I managed to...
Currently, our coqdoc is a complete mess. I don't know how to fix this in a good way, and it's well possible that we want to ignore the issue for...
After discussion with Andrej, here's a proposal how to structure the repository in the future in order to be most easily to maintain. Please add your thoughts from a user...
Andrej's investigation into performance yielded that we shouldn't use `Print Assumptions`, because it is too slow. Now an open question is whether we want `Check` commands after important theorems or...
Regarding the naming definition we started in #41, I did some (limited) research what standard resources call "recursively enumerable". (My opinion then follows below) Rogers: > **Definition** A is recursively...
**Project name:** Coq Library of Complexity proofs **Initial author(s):** Fabian Kunze, Lennard Gäher, Maxi Wuttke, Yannick Forster **Current URL:** https://github.com/uds-psl/coq-library-complexity **Kind:** pure Coq library, formalization of mathematical theorems **License:** CeCill...
This should probably go to a new branch. I also have a version for 8.7 and can file a pull request against the new branch afterwards.