# Library notations

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 "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").