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