-
Notifications
You must be signed in to change notification settings - Fork 18
Description
I created a branch 'doc' in my repo with some notes about the structure of the code.
I’m beginning to decipher Primitives.v
and would like to add my notes about it to this repo, so that other people can understand it more easily.
I’d like to discuss how the documentation shall be added to the repo. Should it be in coqdoc format (adding a new target to the makefile) or in files separate to src/
? Should it, if read front-to-back, touch on every aspect of the repo or only highlight major parts?
The documentation of the stdlib of Coq is relatively sparse, consisting mostly of headings and a sometimes a few lines of text. I don’t think this style would be completely adequate, because the stdlib contains well-known math, while the structure and content of this repo is unfamiliar to a new reader. But for files like Utility/Monads.v
the style of the stdlib seems okay to me.