From 7f100ace3c803323d978debed5705b4e03898669 Mon Sep 17 00:00:00 2001 From: monate Date: Fri, 14 Mar 2003 10:24:09 +0000 Subject: *** empty log message *** git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3767 85f007b7-540e-0410-9357-904b9bb8a0f7 --- ide/FAQ | 27 ++++++++++++++++++--------- 1 file changed, 18 insertions(+), 9 deletions(-) (limited to 'ide/FAQ') diff --git a/ide/FAQ b/ide/FAQ index a410dbe64..e6e022973 100644 --- a/ide/FAQ +++ b/ide/FAQ @@ -19,24 +19,33 @@ 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 +R4) Thanks to the Notation features in Coq, you just need to insert 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). +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. +Copy/Paste might not work. You need to load a file containing these lines or to enter +the "∀" using an input method. As a convenience, you may put these lines in +a utf8.v file and start coqide with : + coqide -l utf8.v + --Second solution : rebind "a" to forall. Under X11, you need to - use +Input Methods: +-First solution : type "2200" to enter a forall in the script widow. + 2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀" + in UTF-8. + 2203 is for exists. See http://www.unicode.org for more. +-Second solution : rebind "a" to forall and "e" to exists. Under X11, you need to + use something like xmodmap -e "keycode 24 = a A F13 F13" + xmodmap -e "keycode 26 = e E F14 F14" and then to add bind "F13" {"insert-at-cursor" ("∀")} + bind "F14" {"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. + Further symbols can be bound on higher Fxx key symbols. + -- cgit v1.2.3