blob: e00131f7b4934056e6bb1744759a9013ab9cc01c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
|
Q1) How to enable Emacs keybindings?
R1: Insert
gtk-key-theme-name = "Emacs"
in your ".coqide-gtk2rc" file. It may be in the current dir
or in $HOME dir. This is done by default.
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 seem not to be available, set to 0.
Q4) How can use 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" := (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).
======================================================================
Copy/Paste from this file will 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
In the ide subdir of Coq sources, you will find a sample utf8.v with some
notations
Input Methods:
-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.
-Second solution : rebind "<AltGr>a" to forall and "<AltGr>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-gtk2rc.
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 bound on higher Fxx key symbols.
|
