coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] coqdoc autoinsert query results
Date: Wed, 4 Mar 2020 12:54:23 -0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f195.google.com
Ironport-phdr: 9a23:wOvUrxA+xnrF90sYgiUpUyQJP3N1i/DPJgcQr6AfoPdwSP38r8bcNUDSrc9gkEXOFd2Crakb26yL6+jJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6i760TlHERLmcAFxO+69ToXVloG80/2405zVeQRBwjSnN+BcNhKz+CzbtsgNgYZhYo83wx3F6i9BceRX3mNlJhSamR/66oGx/YJs2ytVsvMlscVHVPOpLOwDUbVEAWF+YCgO78rxuEybFFfd1j4nSmwT1yFwLU3d9hijB8X+tyL7sqx23yzIZZSnH4BxYiyr6uJQcDGtjS4GMzAj92SO055/iatapFSqoBktmteJMrHQD+J3e+bmRf1fRWdFWZwPBSlIA4f5bo9WSuRYbLseoI76qF8D6xC5AFv0CQ==

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

[Coq-Club] coqdoc autoinsert query results, Abhishek Anand, 03/04/2020
- Message not available
  - [Coq-Club] Fwd: coqdoc autoinsert query results, Jim Fehrle, 03/04/2020
    - Re: [Coq-Club] Fwd: coqdoc autoinsert query results, Théo Zimmermann, 03/04/2020
- Re: [Coq-Club] coqdoc autoinsert query results, Daniel Schepler, 03/05/2020