The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

On Fri, Jan 3, 2014 at 8:46 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

You can do something like

Definition foo' (if_we_had1 : T1) (if_we_had2 : T2) (if_we_had3 : T1 -> T2 -> T3) : T3 := if_we_had3 if_we_had1 if_we_had2.

Definition t1 : T1 := ...

Definition t2 : T2 := ...

Definition t3 : T1 -> T2 -> T3 := ...

Definition foo : T3 := foo' t1 t2 t3.

Is that close to what you want?

Yes, that can be close in many cases. I'll try using it, Thanks.

But, foo' can sometimes take up too

much space and add to overall verbosity.

Alternatively, you could make liberal use of (* begin hide *), etc.

-Jason

On Fri, Jan 3, 2014 at 7:27 PM, Vladimir Voevodsky <vladimir AT ias.edu> wrote:

On Jan 3, 2014, at 6:40 PM, Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

I'm often running into situations where a definition A depends on some definition B and hence
A cannot be defined(in Coq) before defining B.
However, while communicating the idea to humans via coqdoc, a top down explanation is more suitable, i.e. the definition of B would seem boring/useless until the definition of A is shown to motivate it.

Coqdoc does not seem to provide a way to output definitions and the associated comments in an order that is different that the order in which they appear in the .v file.
Is there an easy way to get around this limitation?

Currently, I have to split the .v file such that the definitions of A and B are in different .v files. Then I include the output .tex files of coqdoc in the
desired order in the main .tex file.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

I would suggest that it is a very useful limitation which makes it difficult to hide things from the reader :)

V.