diff options
Diffstat (limited to 'ide/coqide/FAQ')
| -rw-r--r-- | ide/coqide/FAQ | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/ide/coqide/FAQ b/ide/coqide/FAQ new file mode 100644 index 0000000000..c8b0a5d328 --- /dev/null +++ b/ide/coqide/FAQ @@ -0,0 +1,54 @@ + CoqIde FAQ + +Q0) What is CoqIde? +R0: A powerful graphical interface for Coq. See http://coq.inria.fr. for more informations. + +Q1) How to enable Emacs keybindings? +R1: Insert + gtk-key-theme-name = "Emacs" +in your gtkrc file. The location of this file is system-dependent. If you're running +Gnome, you may use the graphical configuration tools. + +Q2) How to enable antialiased fonts? +R2) Set the GDK_USE_XFT variable to 1. This is by default with Gtk >= 2.2. + If some of your fonts are not available, set GDK_USE_XFT to 0. + +Q4) How to use those Forall and Exists pretty symbols? +R4) Thanks to the Notation features in Coq, you just need to insert these + lines in your Coq Buffer : +====================================================================== +Notation "∀ x : t, P" := (forall x:t, P) (at level 200, x ident). +Notation "∃ x : t, P" := (exists x:t, P) (at level 200, x ident). +====================================================================== +Copy/Paste of these lines from this file will not work outside of CoqIde. +You need to load a file containing these lines or to enter the "∀" +using an input method (see Q5). To try it just use "Require utf8" from inside +CoqIde. +To enable these notations automatically start coqide with + coqide -l utf8 +In the ide subdir of Coq library, you will find a sample utf8.v with some +pretty simple notations. + +Q5) How to define an input method for non ASCII symbols? +R5)-First solution : type "<CONTROL><SHIFT>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 codes. +-Second solution : Use an input method editor, such as SCIM or iBus. The latter offers +a module for LaTeX-like inputting. + +Q6) How to customize the shortcuts for menus? +R6) Two solutions are offered: + - Edit $XDG_CONFIG_HOME/coq/coqide.keys by hand or + - If your system allows it, from CoqIde, you may select a menu entry and press the + desired shortcut. + +Q7) What encoding should I use? What is this \x{iiii} in my file? +R7) The encoding option is related to the way files are saved. + Keep it as UTF-8 until it becomes important for you to exchange files + with non UTF-8 aware applications. + If you choose something else than UTF-8, then missing characters will + be encoded by \x{....} or \x{........} where each dot is an hex. digit. + The number between braces is the hexadecimal UNICODE index for the + missing character. + |