The Coq mailing list

[Jim Fehrle <jim.fehrle AT gmail.com>]

There is such a feature for processing the examples that appear in the documentation, part of our Sphinx customization.  For example:

.. coqtop:: reset none

   Parameters (A : Prop) (B: nat -> Prop) (C: Prop).

.. coqtop:: out

   Goal A /\ (exists x:nat, B x /\ C) -> True.

.. coqtop:: all

   intros (a & x & b & c).

"none", "in", "out" control whether to display the input and output.

Perhaps some of this could be adapted for your use case.  No idea how much work that would require.

Jim

On Wed, Mar 4, 2020 at 12:56 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

Is there a way in coqdoc or a similar tool to automatically include query results in the generated document, especially HTML document?

For example, if I have the following source file,

(**

[[ 

Check Nat.add_0_l.

]]

*)

the HTML output should be:

Check Nat.add_0_l.

Nat.add_0_l
     : ∀ n : nat, 0 + n = n

If coqdoc can't do this, some sort of a .v file preprocessor could use coqtop to convert 

(**

[[ 

Check Nat.add_0_l.

]]

*)

 into 

(**

[[ 

Check Nat.add_0_l.

]]

[[

Nat.add_0_l
     : ∀ n : nat, 0 + n = n

]]

*)

before invoking coqdoc?

-- Abhishek

http://www.cs.cornell.edu/~aa755/