A Coq library for domain theory (http://rwd.rdockins.name/domains/)

root / notations.v

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
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
(* Copyright (c) 2014, Robert Dockins *)

(**  Reserved notation declarations gathered in one place to help
     debug parsing problems, etc.
  *)

Reserved Notation "x ≈ y" (at level 70).
Reserved Notation "x ≉ y" (at level 70).
Reserved Notation "x ≤ y" (at level 70).
Reserved Notation "y ≥ x" (at level 70).
Reserved Notation "x ≰ y" (at level 70).
Reserved Notation "y ≱ x" (at level 70).

Reserved Notation "f # x"
  (at level 55, arguments at next level).

Reserved Notation "x ∘ y"
  (at level 40, left associativity,
  format
    "'[hv' x  '∘' '/'  y ']'").

Reserved Notation "〈 f , g 〉" 
  (format
    "'[hv' '〈' f '/' ','  g '/' '〉' ']'"
  ). 

Reserved Notation "《 f , g 》" 
  (format
    "'[hv' '《' f '/' ','  g '/' '》' ']'"
  ). 

Reserved Notation "'Λ' f" 
  (f at next level, at level 0,
  format
    "'[hv' 'Λ' f ']'"
  ).

Reserved Notation "〚 x 〛"
  (format
    "'[hv' '〚'  x  '〛' ']'"
  ). 

Reserved Notation "x ∈ X" (at level 60).
Reserved Notation "x ∉ X"  (at level 60).
Reserved Notation "X ⊆ Y" (at level 66).
Reserved Notation "∪ XS" (at level 50).
Reserved Notation "∅".

Reserved Notation "∐ XS"  (at level 10).
Reserved Notation "⊥".
Reserved Notation "∗".

Reserved Notation "'id'".
Reserved Notation "'id' ( A )" (format "'id' '(' A ')'").
Reserved Notation "'Id'".
Reserved Notation "'Id' ( A )" (format "'Id' '(' A ')'").

Reserved Notation "A → B" (at level 65).
Reserved Notation "A ↣ B" (at level 65).
Reserved Notation "A ↠ B" (at level 65).
Reserved Notation "A ↔ B" (at level 65).

Reserved Notation "'!'".
Reserved Notation "'¡'".

Reserved Notation "f '⁻¹'" (at level 1, format "f '⁻¹'").

Reserved Notation "'ι₁'".
Reserved Notation "'ι₂'".
Reserved Notation "'π₁'".
Reserved Notation "'π₂'".

Reserved Notation "A × B" (at level 54, left associativity).
Reserved Notation "A ⊗ B" (at level 54, left associativity).
Reserved Notation "A ⊕ B" (at level 50, left associativity).

Reserved Notation "A ⇒ B" (at level 35, right associativity).
Reserved Notation "A ⊸ B" (at level 35, right associativity).

Reserved Notation "F ▹ nt" (at level 36).
Reserved Notation "nt ◃ F" (at level 36).

Reserved Notation "‖ x ‖" (at level 20, format "‖ x ‖").
Reserved Notation "a ♯ b" (at level 25, no associativity, format "a ♯ b").
Reserved Notation "u ⇋ v" (at level 20, no associativity).
Reserved Notation "p · x" (at level 35, right associativity, format "p · x").
Reserved Notation "'ν' x , t" (at level 50, format "'ν'  x ,  t").