1 (*********************************************************************************************************************************)
2 (* Notations: miscellaneous notations *)
3 (*********************************************************************************************************************************)
5 Require Import Coq.Unicode.Utf8.
6 Require Import Coq.Classes.RelationClasses.
7 Require Import Coq.Classes.Morphisms.
8 Require Import Coq.Setoids.Setoid.
10 Export Coq.Unicode.Utf8.
11 Export Coq.Classes.RelationClasses.
12 Export Coq.Classes.Morphisms.
13 Export Coq.Setoids.Setoid.
15 Set Printing Width 130. (* Proof General seems to add an extra two columns of overhead *)
16 Generalizable All Variables.
18 Reserved Notation "a ~=> b" (at level 70, right associativity).
19 Reserved Notation "H ===> C" (at level 100).
20 Reserved Notation "f >>=>> g" (at level 45).
21 Reserved Notation "a ~~{ C }~~> b" (at level 100).
22 Reserved Notation "f <--> g" (at level 20).
23 Reserved Notation "! f" (at level 2).
24 Reserved Notation "? f" (at level 2).
25 Reserved Notation "# f" (at level 2).
26 Reserved Notation "f '⁻¹'" (at level 1).
27 Reserved Notation "a ≅ b" (at level 70, right associativity).
28 Reserved Notation "C 'ᵒᴾ'" (at level 1).
29 Reserved Notation "F \ a" (at level 20).
30 Reserved Notation "f >>> g" (at level 45).
31 Reserved Notation "a >>≅>> b" (at level 45).
32 Reserved Notation "a ~~ b" (at level 54).
33 Reserved Notation "a ~> b" (at level 70, right associativity).
34 Reserved Notation "a ≃ b" (at level 70, right associativity).
35 Reserved Notation "a ≃≃ b" (at level 70, right associativity).
36 Reserved Notation "a ~~> b" (at level 70, right associativity).
37 Reserved Notation "F ~~~> G" (at level 70, right associativity).
38 Reserved Notation "F <~~~> G" (at level 70, right associativity).
39 Reserved Notation "F <~~⊗~~> G" (at level 70, right associativity).
40 Reserved Notation "a ⊗ b" (at level 40).
41 Reserved Notation "a ⊗⊗ b" (at level 40).
42 Reserved Notation "a ⊕ b" (at level 40).
43 Reserved Notation "a ⊕⊕ b" (at level 40).
44 Reserved Notation "f ⋉ A" (at level 40).
45 Reserved Notation "A ⋊ f" (at level 40).
46 Reserved Notation "- ⋉ A" (at level 40).
47 Reserved Notation "A ⋊ -" (at level 40).
48 Reserved Notation "a *** b" (at level 40).
49 Reserved Notation "a ---> b" (at level 11, right associativity).
50 Reserved Notation "a <- b" (at level 100, only parsing).
51 Reserved Notation "a :: b" (at level 60, right associativity).
52 Reserved Notation "a ++ b" (at level 60, right associativity).
53 Reserved Notation "f ○ g" (at level 100).
54 Reserved Notation "f >>>> g" (at level 45).
55 Reserved Notation "a >>⊗>> b" (at level 20).
56 Reserved Notation "f **** g" (at level 40).
57 Reserved Notation "C × D" (at level 40).
58 Reserved Notation "C ×× D" (at level 45).
59 Reserved Notation "C ⁽ºᑭ⁾" (at level 1).
61 Reserved Notation "F -| G" (at level 75).
62 Reserved Notation "'ε'".
63 Reserved Notation "'η'".
65 Close Scope nat_scope. (* so I can redefine '1' *)
67 Delimit Scope arrow_scope with arrow.
68 Delimit Scope biarrow_scope with biarrow.
69 Delimit Scope garrow_scope with garrow.
71 Notation "f ○ g" := (fun x => f(g(x))).
72 Notation "a && b" := (if a then b else false).
73 Notation "a || b" := (if a then true else b).
75 Notation "∀ x y z u q , P" := (forall x y z u q , P)
76 (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
78 Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
79 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
81 Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
82 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
84 Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
85 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
87 Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
88 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
90 Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
91 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, right associativity)
93 Notation "∀ x y z u q v a b r s t , P" := (forall x y z u q v a b r s t , P)
94 (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, s ident, t ident,