coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] proof prettifier (was Re: A formalization in Coq of puzzles involving scales and fake coins.)

From: Bas Spitters <b.a.w.spitters AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] proof prettifier (was Re: A formalization in Coq of puzzles involving scales and fake coins.)
Date: Sun, 15 Nov 2015 12:31:58 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=b.a.w.spitters AT gmail.com; spf=Pass smtp.mailfrom=b.a.w.spitters AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f41.google.com
Ironport-phdr: 9a23:hnC7LR23R2x65F6XsmDT+DRfVm0co7zxezQtwd8ZsegRKfad9pjvdHbS+e9qxAeQG96LtrQZ1qGM4ujJYi8p39WoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6kO74TNaIBjjLw09fr2zQd6PyZnqnLrjs7ToICx2xxOFKYtoKxu3qQiD/uI3uqBFbpgL9x3Sv3FTcP5Xz247bXianhL7+9vitMU7q3cYk7sb+sVBSaT3ebgjBfwdVWx+cjN92Mq+nh7aBSCL+3FUBm4Ri19DBxXPxBD8RJb49CXg4LlTwi6faOf/VvgPQTW+86pxU1e8gmEOcSF/63nWltB9lrlzrxeophg5yInRNtLGfMFid7/QKItJDVFKWdxcAmkYWtux

Eelis van der Weegen wrote a small python script that puts twice the
number of spaces as there are open goals. It also does a few other
things.

Also, I heard rumors about a new coqdoc, but dont have any news.

https://github.com/spitters/ssrcorn/blob/master/tools/coqindenter

On Sun, Nov 15, 2015 at 1:12 AM, Jonathan Leivent
<jonikelee AT gmail.com>
wrote:
>
>
> On 11/14/2015 05:46 PM, Gabriel Scherer wrote:
>>
>> ...
>>
>> I see that your proof script do not use billets (- + * { }).
>> Use bullets!
>>
>> ...
>
>
> Does anyone know of a proof prettifier that will add bullets? Now that Coq
> tells you what bullet to use next, it seems like it should be a relatively
> easy thing to write a script to do...
>
> -- Jonathan
>

[Coq-Club] A formalization in Coq of puzzles involving scales and fake coins., Fred Smith, 11/14/2015
- Re: [Coq-Club] A formalization in Coq of puzzles involving scales and fake coins., Gabriel Scherer, 11/14/2015
  - Re: [Coq-Club] A formalization in Coq of puzzles involving scales and fake coins., Fred Smith, 11/14/2015
  - [Coq-Club] proof prettifier (was Re: A formalization in Coq of puzzles involving scales and fake coins.), Jonathan Leivent, 11/15/2015
    - Re: [Coq-Club] proof prettifier (was Re: A formalization in Coq of puzzles involving scales and fake coins.), Bas Spitters, 11/15/2015