XComposeAndNotations

Pierre Letouzey edited this page Oct 27, 2017 · 7 revisions

In Coq, you can use notations to have fancy (and/or more readable) way to write your code in Coq. Here is an example of what you can have:

Set Implicit Arguments.
Record set (A: Type): Type :=
Comprehension {In: A -> Prop}.
Delimit Scope set_scope with set.
Open Scope set_scope.
Notation "{ x : s 'st' P }" :=
 ({|In:=λ (x: s), P|}) (at level 10, x at level 69): set_scope.
Notation "{ x 'st' P }" := ({x:_ st P}) (at level 10, x at level 69): set_scope.
Notation "x ∈ X" := (X.(In) x) (at level 40): set_scope.
Notation "x ∉ X" := (¬(x ∈ X)) (at level 40): set_scope.
Notation "X ⊆ Y" := (∀ x, x ∈ X → x ∈ Y) (at level 40): set_scope.
Notation "X ≡ Y" := (X⊆Y ∧ Y⊆X) (at level 40): set_scope.
Notation "X ∪ Y" := ({x st x ∈ X ∨ x ∈ Y}) (at level 55): set_scope.
Notation "X ∩ Y" := ({x st x ∈ X ∧ x ∈ Y}) (at level 50): set_scope.
Notation "⋃ X" := ({x st ∃ y, x ∈ y ∧ y ∈ X}) (at level 35): set_scope.
Notation "⋂ X" := ({x st ∀ y, y ∈ X → x ∈ y}) (at level 30): set_scope.
Notation "f ⁻¹ Σ" := ({x st (f x) ∈ Σ}) (at level 5): set_scope.
Notation "∁ A" := ({x st x ∉ A}) (at level 5): set_scope.
Definition empty_set (A: Type) := {x: A st ⊥}.
Definition full_set (A: Type) := {x: A st ⊤}.
Notation "₀ s" := (empty_set s) (at level 5): set_scope.
Notation "₁ s" := (full_set s) (at level 5): set_scope.
Definition finite_union {A: Type} (f: nat -> set A) :=
 fix finite_union n :=
 match n with
 | O => ₀A
 | S k => (f k) ∪ (finite_union k)
 end.
Axiom Extensionnality: ∀ (S: Type) (σ1 σ2: set S), σ1 ≡ σ2 → σ1 = σ2.
Class Topology (S: Type): Type :=
{ O: set (set S);
  Hempty: ₀S ∈ O;
  Hall: ₁S ∈ O;
  Hinter: ∀ ω1 ω2, (ω1 ∈ O) → (ω2 ∈ O) → (ω1 ∩ ω2) ∈ O;
  HUNION: ∀ ωs, (∀ ω, (ω ∈ ωs) → (ω ∈ O)) → (⋃ωs) ∈ O
}.
Definition Compact {A: Type} {ΩA: Topology A} a :=
 ∀ os, (a ⊆ ⋃os ∧ (∀ o, (o ∈ os) → (o ∈ O))) →
 ∃ subos, ∃ n, (∀ m, m<n → (subos m) ∈ os) ∧ a ⊆ (finite_union subos n).
Definition Separables {A: Type} {ΩA: Topology A} x y :=
 ∃ ox, ∃ oy,
 ((y ∈ oy) ∧ (oy ∈ O)) ∧
 ((x ∈ ox) ∧ (ox ∈ O)) ∧
 (ox ⊆ ∁oy).
Lemma compacts_are_closed:
 ∀ A {ΩA: Topology A}, (∀ x y, x ≠ y → Separables x y) →
 ∀ a, Compact a → (∁a ∈ O).

It seems cool, but how to have a way to input such a code in (almost) any editor under X? A good way is to have a "XIM" compliant editor (under X, almost any editor is XIM compliant; so it is the case for emacs, xterm, url in firefox, …), then following some tutorials on XCompose, you can have some cool stuff:

echo 'GTK_IM_MODULE=xim' >> $PROFILE
echo 'QT_IM_MODULE=xim' >> $PROFILE
echo 'XMODIFIERS=@im=xim' >> $PROFILE

where $PROFILE is "/.profile" or "/.xinitrc" (or any script file run at logging time under X).

Now, if you do not have a "<Multi-key>", it can be (although not necessary) to define one:

echo 'keycode 117 = Multi_key' >> ~/.Xmodmap

To know the keycode you want, you can use xev.

Now create or edit "~/.XCompose" to have your wished compositions:

echo 'include "~/.XCompose.my_symbols"' >> ~/.XCompose
touch ~/.XCompose.my_symbols

Now, you have to edit this file to have your own compositions. Take a look at the official webpage of unicode to find the unicode codes you want.

The expected format is:

[non_empty_list_of_keys_or_unicode_name] : [optional """utf8-encoded-character"""] [optional unicode-name] [optional "U"unicode-code]

for instance:

echo '<Multi_key> <a> <l> <l> : "∀" U2200' >> ~/.XCompose.my_symbols

Finally restart your X server, and all should work.

See this file for an example.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.