helm/software/matita/contribs/procedural/Coq/Init/Notations.mma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 include "Coq.ma".
  18
  19 (*#***********************************************************************)
  20
  21 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
  22
  23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
  24
  25 (*   \VV/  **************************************************************)
  26
  27 (*    //   *      This file is distributed under the terms of the       *)
  28
  29 (*         *       GNU Lesser General Public License Version 2.1        *)
  30
  31 (*#***********************************************************************)
  32
  33 (*i $Id: Notations.v,v 1.24.2.2 2004/08/01 09:36:44 herbelin Exp $ i*)
  34
  35 (*#* These are the notations whose level and associativity are imposed by Coq *)
  36
  37 (*#* Notations for propositional connectives *)
  38
  39 (* NOTATION
  40 Reserved Notation "x <-> y" (at level 95, no associativity).
  41 *)
  42
  43 (* NOTATION
  44 Reserved Notation "x /\ y" (at level 80, right associativity).
  45 *)
  46
  47 (* NOTATION
  48 Reserved Notation "x \/ y" (at level 85, right associativity).
  49 *)
  50
  51 (* NOTATION
  52 Reserved Notation "~ x" (at level 75, right associativity).
  53 *)
  54
  55 (*#* Notations for equality and inequalities *)
  56
  57 (* NOTATION
  58 Reserved Notation "x = y  :> T"
  59 (at level 70, y at next level, no associativity).
  60 *)
  61
  62 (* NOTATION
  63 Reserved Notation "x = y" (at level 70, no associativity).
  64 *)
  65
  66 (* NOTATION
  67 Reserved Notation "x = y = z"
  68 (at level 70, no associativity, y at next level).
  69 *)
  70
  71 (* NOTATION
  72 Reserved Notation "x <> y  :> T"
  73 (at level 70, y at next level, no associativity).
  74 *)
  75
  76 (* NOTATION
  77 Reserved Notation "x <> y" (at level 70, no associativity).
  78 *)
  79
  80 (* NOTATION
  81 Reserved Notation "x <= y" (at level 70, no associativity).
  82 *)
  83
  84 (* NOTATION
  85 Reserved Notation "x < y" (at level 70, no associativity).
  86 *)
  87
  88 (* NOTATION
  89 Reserved Notation "x >= y" (at level 70, no associativity).
  90 *)
  91
  92 (* NOTATION
  93 Reserved Notation "x > y" (at level 70, no associativity).
  94 *)
  95
  96 (* NOTATION
  97 Reserved Notation "x <= y <= z" (at level 70, y at next level).
  98 *)
  99
 100 (* NOTATION
 101 Reserved Notation "x <= y < z" (at level 70, y at next level).
 102 *)
 103
 104 (* NOTATION
 105 Reserved Notation "x < y < z" (at level 70, y at next level).
 106 *)
 107
 108 (* NOTATION
 109 Reserved Notation "x < y <= z" (at level 70, y at next level).
 110 *)
 111
 112 (*#* Arithmetical notations (also used for type constructors) *)
 113
 114 (* NOTATION
 115 Reserved Notation "x + y" (at level 50, left associativity).
 116 *)
 117
 118 (* NOTATION
 119 Reserved Notation "x - y" (at level 50, left associativity).
 120 *)
 121
 122 (* NOTATION
 123 Reserved Notation "x * y" (at level 40, left associativity).
 124 *)
 125
 126 (* NOTATION
 127 Reserved Notation "x / y" (at level 40, left associativity).
 128 *)
 129
 130 (* NOTATION
 131 Reserved Notation "- x" (at level 35, right associativity).
 132 *)
 133
 134 (* NOTATION
 135 Reserved Notation "/ x" (at level 35, right associativity).
 136 *)
 137
 138 (* NOTATION
 139 Reserved Notation "x ^ y" (at level 30, right associativity).
 140 *)
 141
 142 (*#* Notations for pairs *)
 143
 144 (* NOTATION
 145 Reserved Notation "( x , y , .. , z )" (at level 0).
 146 *)
 147
 148 (*#* Notation "{ x }" is reserved and has a special status as component
 149     of other notations; it is at level 0 to factor with {x:A|P} etc *)
 150
 151 (* NOTATION
 152 Reserved Notation "{ x }" (at level 0, x at level 99).
 153 *)
 154
 155 (*#* Notations for sum-types *)
 156
 157 (* NOTATION
 158 Reserved Notation "{ A } + { B }" (at level 50, left associativity).
 159 *)
 160
 161 (* NOTATION
 162 Reserved Notation "A + { B }" (at level 50, left associativity).
 163 *)
 164
 165 (*#* Notations for sigma-types or subsets *)
 166
 167 (* NOTATION
 168 Reserved Notation "{ x : A  |  P }" (at level 0, x at level 99).
 169 *)
 170
 171 (* NOTATION
 172 Reserved Notation "{ x : A  |  P  &  Q }" (at level 0, x at level 99).
 173 *)
 174
 175 (* NOTATION
 176 Reserved Notation "{ x : A  &  P }" (at level 0, x at level 99).
 177 *)
 178
 179 (* NOTATION
 180 Reserved Notation "{ x : A  &  P  &  Q }" (at level 0, x at level 99).
 181 *)
 182
 183 (* UNEXPORTED
 184 Delimit Scope type_scope with type.
 185 *)
 186
 187 (* UNEXPORTED
 188 Delimit Scope core_scope with core.
 189 *)
 190
 191 (* UNEXPORTED
 192 Open Scope core_scope.
 193 *)
 194
 195 (* UNEXPORTED
 196 Open Scope type_scope.
 197 *)
 198