Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Re: [coqdev] What about a Coq ExtLib ?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Re: [coqdev] What about a Coq ExtLib ?


chronological Thread 
  • From: Frederic Blanqui <frederic.blanqui AT inria.fr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Re: [coqdev] What about a Coq ExtLib ?
  • Date: Mon, 21 Mar 2011 09:42:36 +0800



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.



Archive powered by MhonArc 2.6.16.

Top of Page