The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Le 19/03/2011 23:57, Daniel Schepler a écrit :
> 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.
I don't think that the guideline should specify what should be provided 
or not. Both lemmas are interesting (with impl and iff). The problem is 
perhaps rather to agree on a naming convention.