XComposeAndNotations - coq/coq GitHub Wiki

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.

To the extent possible under law, the contributors of β€œCocorico!, the Coq wiki” have waived all copyright and related or neighboring rights to their contributions.

CC0

By contributing to Cocorico!, the Coq wiki, you agree that you hold the copyright and you agree to license your contribution under the CC0 license or you agree that you have permission to distribute your contribution under the CC0 license.

⚠️ **GitHub.com Fallback** ⚠️