Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Tricks to make Unicode input easier and proof scripts more readable (was Re: Lean Theorem Prover)

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:

1. Is it possible to disable subscripting? I have many identifiers of the form c_n, where c is a string and n a number that I don't want to be displayed as a subscript.
2. Can comments be prettified?
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?

Thank you,
Lucian

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.





Archive powered by MHonArc 2.6.18.

Top of Page