matita/matita/contribs/lambdadelta/apps_2/etc/MLTT1/notation.etc

   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 (* NOTATION FOR MARTIN-LÖF TYPE THEORY WITH ONE UNIVERSE (MLTT1) ************)
  16
  17 (* Syntax extension *********************************************************)
  18
  19 notation "hvbox( □ )"
  20  non associative with precedence 90
  21  for @{ 'Box }.
  22
  23 notation "hvbox(T1 break ⤏ T2)"
  24   right associative with precedence 65
  25   for @{ 'TImp $T1 $T2 }.
  26
  27 notation "hvbox( L break Λ T )"
  28  left associative with precedence 60
  29  for @{ 'LAbst $L $T }.
  30
  31 notation "hvbox( L break Δ T )"
  32  left associative with precedence 60
  33  for @{ 'LAbbr $L $T }.
  34
  35 notation "hvbox( Λ T )"
  36  non associative with precedence 65
  37  for @{ 'TAbst $T }.
  38
  39 (* Primitive global constants ***********************************************)
  40
  41 notation "hvbox( 𝔼 )"
  42  non associative with precedence 90
  43  for @{ 'Empty }.
  44
  45 notation "hvbox( 𝕖𝕣 [ T ] )"
  46  non associative with precedence 90
  47  for @{ 'ERec $T }.
  48
  49 notation "hvbox( 𝕆 )"
  50  non associative with precedence 90
  51  for @{ 'One }.
  52
  53 notation "hvbox( 𝕥 )"
  54  non associative with precedence 90
  55  for @{ 'TT }.
  56
  57 notation "hvbox( 𝕠𝕣 [ T1 , break T2 ] )"
  58  non associative with precedence 90
  59  for @{ 'ORec $T1 $T2 }.
  60 (*
  61 notation "hvbox( ℕ )"
  62  non associative with precedence 90
  63  for @{ 'Nat }.
  64
  65 notation "hvbox( 𝕫 )"
  66  non associative with precedence 90
  67  for @{ 'Zero }.
  68
  69 notation "hvbox( 𝕤 [ T ] )"
  70  non associative with precedence 90
  71  for @{ 'Succ $T }.
  72
  73 notation "hvbox( 𝕟𝕣 [ T1 , break T2 , break T3 ] )"
  74  non associative with precedence 90
  75  for @{ 'NRec $T1 $T2 $3 }.
  76 *)
  77 notation "hvbox( T1 ⊕ T2 )"
  78  left associative with precedence 70
  79  for @{ 'Sum $T1 $T2 }.
  80
  81 notation "hvbox( 𝕤𝕟 [ T ] )"
  82  non associative with precedence 90
  83  for @{ 'Sn $T }.
  84
  85 notation "hvbox( 𝕕𝕩 [ T ] )"
  86  non associative with precedence 90
  87  for @{ 'Dx $T }.
  88
  89 notation "hvbox( 𝕤𝕣 [ T1 , break T2 , break T3 ] )"
  90  non associative with precedence 90
  91  for @{ 'SRec $T1 $T2 $3 }.
  92 (*
  93 notation "hvbox( 𝕌 )"
  94  non associative with precedence 90
  95  for @{ 'Univ }.
  96
  97 notation "hvbox( 𝕖 )"
  98  non associative with precedence 90
  99  for @{ 'UE }.
 100
 101 notation "hvbox( 𝕠 )"
 102  non associative with precedence 90
 103  for @{ 'UO }.
 104
 105 notation "hvbox( 𝕟 )"
 106  non associative with precedence 90
 107  for @{ 'UN }.
 108 *)