update submodule pointer

[coq-hetmet.git] / src / Preamble.v

diff --git a/src/Preamble.v b/src/Preamble.v
index 026d6d1..453027a 100644 (file)
--- a/src/Preamble.v
+++ b/src/Preamble.v
@@ -16,8 +16,11 @@ Export Coq.Setoids.Setoid.
 Set Printing Width 130.       (* Proof General seems to add an extra two columns of overhead *)
 Generalizable All Variables.
 
+Reserved Notation "a ** b"                      (at level 40).
+Reserved Notation "a ;; b"                      (at level 45).
+
 Reserved Notation "a -~- b"                     (at level 10).
-Reserved Notation "a ** b"                      (at level 10).
+Reserved Notation "pf1 === pf2"                 (at level 80).
 Reserved Notation "?? x"                        (at level 1).
 Reserved Notation "a ,, b"                      (at level 50).
 Reserved Notation "!! f"                        (at level 3).
@@ -52,7 +55,6 @@ Reserved Notation "A ⋊ f"                       (at level 40).
 Reserved Notation "- ⋉ A"                       (at level 40).
 Reserved Notation "A ⋊ -"                       (at level 40).
 Reserved Notation "a *** b"                     (at level 40).
-Reserved Notation "a ;; b"                      (at level 45).
 Reserved Notation "[# f #]"                     (at level 2).
 Reserved Notation "a ---> b"                    (at level 11, right associativity).
 Reserved Notation "a <- b"                      (at level 100, only parsing).
@@ -69,7 +71,6 @@ Reserved Notation "f ○ g"                       (at level 100).
 Reserved Notation "a ==[ n ]==> b"              (at level 20).
 Reserved Notation "a ==[ h | c ]==> b"          (at level 20).
 Reserved Notation "H /⋯⋯/ C"                    (at level 70).
-Reserved Notation "pf1 === pf2"                 (at level 80).
 Reserved Notation "a |== b @@ c"                (at level 100).
 Reserved Notation "f >>>> g"                    (at level 45).
 Reserved Notation "a >>[ n ]<< b"               (at level 100).
@@ -85,13 +86,13 @@ Reserved Notation "Γ '∌∌'   x"                  (at level 10).
 Reserved Notation "Γ '∋∋'   x : a ∼ b"          (at level 10, x at level 99).
 Reserved Notation "Γ '∋'    x : c"              (at level 10, x at level 99).
 
-Reserved Notation "a ⇛ b"                       (at level 40).
+Reserved Notation "a ⇛ b"                       (at level 55, right associativity).
 Reserved Notation "φ₁ →→ φ₂"                    (at level 11, right associativity).
 Reserved Notation "a '⊢ᴛy'  b : c"              (at level 20, b at level 99, c at level 80).
 Reserved Notation "a '⊢ᴄᴏ'  b : c ∼ d"          (at level 20, b at level 99).
 Reserved Notation "Γ '+'    x : c"              (at level 50, x at level 99).
 Reserved Notation "Γ '++'   x : a ∼ b"          (at level 50, x at level 99).
-Reserved Notation "φ₁ ∼∼ φ₂ : κ ⇒ φ₃"           (at level 11, φ₂ at level 99, right associativity).
+Reserved Notation "φ₁ ∼∼ φ₂ ⇒ φ₃"               (at level 11, φ₂ at level 99, right associativity).
 
 Reserved Notation "Γ > past : present '⊢ᴇ' succedent"
    (at level 52, past at level 99, present at level 50, succedent at level 50).
@@ -100,7 +101,6 @@ Reserved Notation "'η'".
 Reserved Notation "'ε'".
 Reserved Notation "'★'".
 
-Notation "a +++ b" := (append a b) (at level 100).
 Close Scope nat_scope.  (* so I can redefine '1' *)
 
 Delimit Scope arrow_scope   with arrow.
@@ -109,6 +109,8 @@ Delimit Scope garrow_scope  with garrow.
 
 Notation "f ○ g"    := (fun x => f(g(x))).
 Notation "?? T"     := (option T).
+Notation "a && b"   := (if a then b else false).
+Notation "a || b"   := (if a then true else b).
 
 (* these are handy since Coq's pattern matching syntax isn't integrated with its abstraction binders (like Haskell and ML) *)
 Notation "'⟨' x ',' y '⟩'" := ((x,y)) (at level 100).