Niels van der Weide
Niels van der Weide
The author of the file is @Kfwullaert , so he is most likely to know.
> We all known that coq `-type-in-type` is inconsistent, in README the author says "we continue to keep track of universe levels in these files 'by hand'". Do we have...
> @arnoudvanderleer : each version of the coqdoc is many MB big. I wonder how quickly a repository hosting the documentation for each merged PR to UniMath would grow -...
> No, we do not; it would be nice to do it. The suggestion by Arnoud would give a way to display the documentation of the latest version of UniMath....
UniMath is backed up on Zenodo. Whenever a new tag is made, a new version of UniMath is added to Zenodo. See: https://zenodo.org/records/10900429. Zenodo gives permanent storage and a doi....
It is a warning, right? So, it should compile, but it says that the notation won't be printed. What about adding ` : only parsing`? That should be semantically equivalent.
> That would solve the warning. Although I added this notation mainly for printing 😅 Sure. The warning does suggest that it is not printed, so it might be that...
This PR is work in progress, right? If so, could you mark it as a draft to make that clear?
I think that the most important information should be in `.md` files, and that the wiki should only be supplementary information. If I look for something, then I check `.md`...
The following are subsets: Most important: - Installation instructions - Style guide - Links to Zulip - Citation and link to Zenodo Supplementary material: - Exact formulation of the resizing...