Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Guidelines

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Guidelines


chronological Thread 
  • From: AUGER Cedric <Cedric.Auger AT lri.fr>
  • Cc: coq-club AT inria.fr
  • Subject: [Coq-Club] Guidelines
  • Date: Mon, 21 Mar 2011 09:39:34 +0100

I started this thread since some of us were talking about guidelines
and the standard library more than a Coq-Extlib.

About the type conventions, I would like to know your point of view
with this:

Is it better to have:

(1) âˆ€ A B, P A â†’ Q B â†’ R

or:

(2) âˆ€ A, P A â†’ âˆ€ B, Q B â†’ R

A lot of people use (1), but I have always found (2) better, in
particular in combination with "Set Implicit Arguments.".

(There could also be the Higher order point of view
 "(λ B· (1) A B PA): âˆ€ B, Q B â†’ R" is not as nice as
 "(2) A PA: âˆ€ B, Q B â†’ R";

 but it is versus:
 "(1) A B: P A â†’ Q B â†’ R" which is nicer than
 "λ PA· (2) A PA B: P A â†’ Q B â†’ R"

 I happen to use the first case more often, so it gives me another
 advantage of this order.)

Same things appear for constructors:

Inductive R: Prop :=
R_intro:  âˆ€ A B, P A â†’ Q B â†’ R.

versus

Inductive R: Prop :=
R_intro: âˆ€ A, P A â†’ âˆ€ B, Q B â†’ R.

I also think that most of the tactics work better with the (2) form
than with the (1), since there are some cases where "B" must be guessed
in (1).

So if I would add something to guidelines I would also add the (1) form;
but I think most people prefer to add the dependant parameters first
(there is a "forall" less to type, and people prefer to introduce all
the general context first).




Archive powered by MhonArc 2.6.16.

Top of Page