coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Coq and RSI

From: Stefan Monnier <monnier AT IRO.UMontreal.CA>
To: "J. Ian Johnson" <ianj AT ccs.neu.edu>
Cc: Thomas Braibant <thomas.braibant AT gmail.com>, coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Coq and RSI
Date: Tue, 28 Aug 2012 16:03:54 -0400

> (define-key coq-mode-map (kbd "-") '(lambda () (interactive) (insert
> "_")))
> (define-key coq-mode-map (kbd "_") '(lambda () (interactive) (insert
> "-"))))

BTW, those (lambda ..) sexps are functions (rather than mere data)
so don't quote them.

Stefan

[Coq-Club] Coq and RSI, Thomas Braibant, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Kristopher Micinski, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Enrico Tassi, 08/28/2012
- Re: [Coq-Club] Coq and RSI, J. Ian Johnson, 08/28/2012
  - Re: [Coq-Club] Coq and RSI, Stefan Monnier, 08/28/2012
- Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/29/2012
- <Possible follow-up(s)>
- Re: [Coq-Club] Coq and RSI, J. Ian Johnson, 08/28/2012
  - Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/29/2012
    - Re: [Coq-Club] Coq and RSI, Thomas Braibant, 08/29/2012
      - Re: [Coq-Club] Coq and RSI, Joseph Tassarotti, 08/29/2012
      - Re: [Coq-Club] Coq and RSI, Pierre Courtieu, 08/30/2012