The Coq mailing list

[Yucheng Zhang <yczhang89 AT gmail.com>]

Note that in my last mail, the mentioned 'coqdoc' and 'coq2html' does not hide
definition of functions..

On Jun 21, 2013, at 6:47 PM, Math Prover 
<mathprover AT gmail.com>
 wrote:
> I'm okay with both of the above. Is there anyway to have what I want
> above? (mainly, I want a single place where all the Functions / Lemmas
> so that when I'm searching for a particular function/lemma, I can only
> look through the declarations without seeing the proofs).

Modules can be used for this purpose: use a Module Type for the declarations
and then a Module implements that module type. An example goes as follows:

Module Type A.
  Parameter f : nat -> nat.
  Axiom f_0 : forall x, f x = x + 1.
End A.

Module ImplA <: A.
  Definition f x := x + 1.

  Lemma f_0 : forall x, f x = x + 1.
  Proof.
    auto.
  Qed.
End ImplA.