coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
Chronological Thread
- From: "Lucian M. Patcas" <lucian.patcas AT gmail.com>
- To: coq-club <coq-club AT inria.fr>, clement.pit AT gmail.com
- Subject: Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)
- Date: Thu, 3 Mar 2016 23:59:21 -0500
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lucian.patcas AT gmail.com; spf=Pass smtp.mailfrom=lucian.patcas AT gmail.com; spf=None smtp.helo=postmaster AT mail-pa0-f52.google.com
- Ironport-phdr: 9a23:mdBTiB96/laPOP9uRHKM819IXTAuvvDOBiVQ1KB91OMcTK2v8tzYMVDF4r011RmSDdqdtK8P1LuempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRciN0o/ohqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwu3cYh/V0/MlZFK7+Yq5wGbdfFXEtN30/zMztrxjKCwWVsD9UWWEblxdOH07d7Q3SUZL4sy+8ve14iweAOsijB5QpUjWr6e9ODlfQgTsMPiVzuDXTl8dxhaQduBu9rBVk64HRaYCRcvF5e/WOLpshWWNdU5MJBGR6CYSmYt5XAg==
Hi Clément,
I've been playing with company-coq for a few days and have a few questions:
3. Is it possible to generate prettified coqdoc documents?
4. I don't want Prop, bool etc to be prettified. What file do I have to edit to remove this behaviour?
On 3 March 2016 at 11:42, Clément Pit--Claudel <clement.pit AT gmail.com> wrote:
I think prettification offers an interesting middle ground (see an example at https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts; these two screenshots show the same Emacs buffer, with and without the prettification layer). This should allow both kinds of SW engineers to work on the same files.
Clément.
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), (continued)
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Ralf Jung, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/02/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre-Marie Pédrot, 03/02/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Gabriel Scherer, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Enrico Tassi, 03/03/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Jonathan Leivent, 03/03/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Lucian M. Patcas, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/04/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/06/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/04/2016
- RE: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Soegtrop, Michael, 03/09/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Pierre Courtieu, 03/11/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Gabriel Scherer, 03/11/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/11/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/11/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Clément Pit--Claudel, 03/11/2016
- Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover), Jonathan Leivent, 03/11/2016
Archive powered by MHonArc 2.6.18.