From 64f0fe542c3871d76eddf520b307ecd0a0634e89 Mon Sep 17 00:00:00 2001 From: monate Date: Mon, 10 Mar 2003 19:16:28 +0000 Subject: coqide: maj des bindings git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3752 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/FAQ | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) (limited to 'ide/FAQ') diff --git a/ide/FAQ b/ide/FAQ index 2d7d39bf5b..a410dbe64a 100644 --- a/ide/FAQ +++ b/ide/FAQ @@ -17,3 +17,26 @@ R2) Insert Q3) How to enable antialiased fonts? R3) Set the GDK_USE_XFT variable to 1. + +Q4) How can use Forall and Exists pretty symbols ? +R4) Thanks to the Notation features in Coq, you just need to paste these + lines in your Coq Buffer : +====================================================================== +Notation "∀ x : t | P" := (x:t)P (at level 1, x,t,P at level 10). +Notation "~ x : t | P" := (EXT x:t|P) (at level 1, x,t,P at level 10). +====================================================================== +Then you need an input method for these symbols. +-First solution : type "2200" to enter a forall. 2200 is the + hexadecimal code for forall in unicode charts. + 2203 is for exists. See http://www.unicode.org for more. + +-Second solution : rebind "a" to forall. Under X11, you need to + use + xmodmap -e "keycode 24 = a A F13 F13" + and then to add + bind "F13" {"insert-at-cursor" ("∀")} + to your "binding "text"" section in .coqiderc. + The strange ("∀") argument is the UTF-8 encoding for + 0x2200. It is computed by lablgtk2 by + Glib.Utf8.from_unichar 0x2200;; + Further symbols can be found on higher Fxx key symbols. -- cgit v1.2.3