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?
note that, with iff, you can also use rewrite, which is quite nice.