-Notation "f ○ g" := (fun x => f(g(x))).
-Notation "?? T" := (option T).
-Notation "a && b" := (if a then b else false).
-
-(* 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).
-Notation "'Λ' '⟨' x ',' y '⟩' e" := (fun xy => match xy with (a,b) => (fun x y => e) a b end) (at level 100).
-Notation "'Λ' '⟨' x ',' '⟨' y ',' z '⟩' '⟩' e" :=
- (fun xyz => match xyz with (a,bc) => match bc with (b,c) => (fun x y z => e) a b c end end) (at level 100).
-Notation "'Λ' '⟨' '⟨' x ',' y '⟩' ',' z '⟩' e" :=
- (fun xyz => match xyz with (ab,c) => match ab with (a,b) => (fun x y z => e) a b c end end) (at level 100).
-
-Notation "∀ x y z u q , P" := (forall x y z u q , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v , P" := (forall x y z u q v , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a , P" := (forall x y z u q v a , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b , P" := (forall x y z u q v a b , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b r , P" := (forall x y z u q v a b r , P)
- (at level 200, q ident, x ident, y ident, z ident, u ident, v ident, a ident, b ident, r ident, right associativity)
- : type_scope.
-Notation "∀ x y z u q v a b r s , P" := (forall x y z u q v a b r s , P)
- (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)
- : type_scope.
-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)
- (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,
- right associativity)
- : type_scope.