src/Notations.v

   1 (*********************************************************************************************************************************)
   2 (* Notations: miscellaneous notations                                                                                             *)
   3 (*********************************************************************************************************************************)
   4
   5 Require Import Coq.Unicode.Utf8.
   6 Require Import Coq.Classes.RelationClasses.
   7 Require Import Coq.Classes.Morphisms.
   8 Require Import Coq.Setoids.Setoid.
   9 Require Setoid.
  10 Export Coq.Unicode.Utf8.
  11 Export Coq.Classes.RelationClasses.
  12 Export Coq.Classes.Morphisms.
  13 Export Coq.Setoids.Setoid.
  14
  15 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
  16 Generalizable All Variables.
  17
  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 54).
  32 Reserved Notation "a ~> b"                      (at level 70, right associativity).
  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 "F  ~~~> G"                   (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 "a ⊗ b"                       (at level 40).
  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 "f ⋉ A"                       (at level 40).
  44 Reserved Notation "A ⋊ f"                       (at level 40).
  45 Reserved Notation "- ⋉ A"                       (at level 40).
  46 Reserved Notation "A ⋊ -"                       (at level 40).
  47 Reserved Notation "a *** b"                     (at level 40).
  48 Reserved Notation "a ---> b"                    (at level 11, right associativity).
  49 Reserved Notation "a <- b"                      (at level 100, only parsing).
  50 Reserved Notation "a :: b"                      (at level 60, right associativity).
  51 Reserved Notation "a ++ b"                      (at level 60, right associativity).
  52 Reserved Notation "f ○ g"                       (at level 100).
  53 Reserved Notation "f >>>> g"                    (at level 45).
  54 Reserved Notation "f **** g"                    (at level 40).
  55 Reserved Notation "C × D"                       (at level 40).
  56 Reserved Notation "C ×× D"                      (at level 45).
  57 Reserved Notation "C ⁽ºᑭ⁾"                      (at level 1).
  58
  59 Reserved Notation "F -| G"                      (at level 75).
  60 Reserved Notation "'ε'".
  61 Reserved Notation "'η'".
  62
  63 Close Scope nat_scope.  (* so I can redefine '1' *)
  64
  65 Delimit Scope arrow_scope   with arrow.
  66 Delimit Scope biarrow_scope with biarrow.
  67 Delimit Scope garrow_scope  with garrow.
  68
  69 Notation "f ○ g"    := (fun x => f(g(x))).
  70 Notation "a && b"   := (if a then b else false).
  71 Notation "a || b"   := (if a then true else b).
  72
  73 Notation "∀ x y z u q , P" := (forall x y z u q , P)
  74   (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
  75   : type_scope.
  76 Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
  77   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
  78   : type_scope.
  79 Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
  80   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
  81   : type_scope.
  82 Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
  83   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
  84   : type_scope.
  85 Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
  86   (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
  87   : type_scope.
  88 Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
  89   (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)
  90   : type_scope.
  91 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)
  92   (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,
  93     right associativity)
  94   : type_scope.