The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Thursday 17 March 2011 13:21:46 Hugo Herbelin wrote:
> Nevertheless, I started to make public on Cocorico a set of tentative
> guidelines that "we" expect users to follow before submitting an
> addition or a modification to a library. I put the text on the wiki
> (page http://coq.inria.fr/cocorico/HowToContributeToTheStandardLibrary)
> so that anyone can discuss the guidelines, add new questions about
> unclear or missing recommendations, comment about whether such or such
> guideline is reasonable or not, etc. I hope that at some time, we will
> have converged to something comprehensive and useful for everyone.

How about a guideline that authors should use Type wherever possible instead 
of restricting themselves to Set?  (With an obvious exception for declaring 
the universe of an inductive type with no input types.)

Also, I've found that as a practical matter, it's more difficult to use "if 
and 
only if" results than the equivalent pair of split results, because "apply 
->" 
and "apply <-" aren't as good at unification as the stock "apply" (in 
particular they don't accept "with" specifiers).  Is this something that 
should 
be mentioned in the guidelines, to split up "if and only if" results?

There are several support parts of my recent ZornsLemma contribution that I 
think would make good general additions to the standard library once they're 
reformatted to the guidelines -- although I'm in the process of revising much 
of it to take advantage of type classes, and in particular I'm completely 
rewriting FiniteTypes and CountableTypes with more computationally oriented 
definitions involving iterator functions.
-- 
Daniel Schepler