Commit 30f481c2 by Robbert

Merge branch 'stdpp_scope' into 'master'

Use `stdpp_scope` for all notations. See merge request !17
parents c92654ed 4b73a5c1
Pipeline #5280 passed with stages
in 14 minutes 25 seconds
......@@ -92,10 +92,10 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
(R : relation A) : relation (M A) := map_relation R (λ _, False) (λ _, True).
Definition map_disjoint `{ A, Lookup K A (M A)} {A} : relation (M A) :=
map_relation (λ _ _, False) (λ _, True) (λ _, True).
Infix "##ₘ" := map_disjoint (at level 70) : C_scope.
Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
Hint Extern 0 (_ ## _) => symmetry; eassumption.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : C_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ## m) (only parsing) : C_scope.
Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
Notation "(.##ₘ m )" := (λ m2, m2 ## m) (only parsing) : stdpp_scope.
Instance map_subseteq `{ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
map_included (=).
......
......@@ -30,21 +30,21 @@ Arguments Permutation {_} _ _ : assert.
Arguments Forall_cons {_} _ _ _ _ _ : assert.
Remove Hints Permutation_cons : typeclass_instances.
Notation "(::)" := cons (only parsing) : C_scope.
Notation "( x ::)" := (cons x) (only parsing) : C_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : C_scope.
Notation "(++)" := app (only parsing) : C_scope.
Notation "( l ++)" := (app l) (only parsing) : C_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : C_scope.
Infix "≡ₚ" := Permutation (at level 70, no associativity) : C_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : C_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : C_scope.
Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : C_scope.
Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : C_scope.
Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : C_scope.
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : C_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : C_scope.
Notation "(::)" := cons (only parsing) : stdpp_scope.
Notation "( x ::)" := (cons x) (only parsing) : stdpp_scope.
Notation "(:: l )" := (λ x, cons x l) (only parsing) : stdpp_scope.
Notation "(++)" := app (only parsing) : stdpp_scope.
Notation "( l ++)" := (app l) (only parsing) : stdpp_scope.
Notation "(++ k )" := (λ l, app l k) (only parsing) : stdpp_scope.
Infix "≡ₚ" := Permutation (at level 70, no associativity) : stdpp_scope.
Notation "(≡ₚ)" := Permutation (only parsing) : stdpp_scope.
Notation "( x ≡ₚ)" := (Permutation x) (only parsing) : stdpp_scope.
Notation "(≡ₚ x )" := (λ y, y ≡ₚ x) (only parsing) : stdpp_scope.
Notation "(≢ₚ)" := (λ x y, ¬x ≡ₚ y) (only parsing) : stdpp_scope.
Notation "x ≢ₚ y":= (¬x ≡ₚ y) (at level 70, no associativity) : stdpp_scope.
Notation "( x ≢ₚ)" := (λ y, x ≢ₚ y) (only parsing) : stdpp_scope.
Notation "(≢ₚ x )" := (λ y, y ≢ₚ x) (only parsing) : stdpp_scope.
Instance maybe_cons {A} : Maybe2 (@cons A) := λ l,
match l with x :: l => Some (x,l) | _ => None end.
......@@ -240,8 +240,8 @@ Fixpoint permutations {A} (l : list A) : list (list A) :=
The predicate [prefix] holds if the first list is a prefix of the second. *)
Definition suffix {A} : relation (list A) := λ l1 l2, k, l2 = k ++ l1.
Definition prefix {A} : relation (list A) := λ l1 l2, k, l2 = l1 ++ k.
Infix "`suffix_of`" := suffix (at level 70) : C_scope.
Infix "`prefix_of`" := prefix (at level 70) : C_scope.
Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
Hint Extern 0 (_ `prefix_of` _) => reflexivity.
Hint Extern 0 (_ `suffix_of` _) => reflexivity.
......@@ -271,7 +271,7 @@ Inductive sublist {A} : relation (list A) :=
| sublist_nil : sublist [] []
| sublist_skip x l1 l2 : sublist l1 l2 sublist (x :: l1) (x :: l2)
| sublist_cons x l1 l2 : sublist l1 l2 sublist l1 (x :: l2).
Infix "`sublist_of`" := sublist (at level 70) : C_scope.
Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
Hint Extern 0 (_ `sublist_of` _) => reflexivity.
(** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
......@@ -282,7 +282,7 @@ Inductive submseteq {A} : relation (list A) :=
| submseteq_swap x y l : submseteq (y :: x :: l) (x :: y :: l)
| submseteq_cons x l1 l2 : submseteq l1 l2 submseteq l1 (x :: l2)
| submseteq_trans l1 l2 l3 : submseteq l1 l2 submseteq l2 l3 submseteq l1 l3.
Infix "⊆+" := submseteq (at level 70) : C_scope.
Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
Hint Extern 0 (_ + _) => reflexivity.
(** Removes [x] from the list [l]. The function returns a [Some] when the
......
......@@ -9,7 +9,7 @@ Add Printing Constructor set.
Arguments mkSet {_} _ : assert.
Arguments set_car {_} _ _ : assert.
Notation "{[ x | P ]}" := (mkSet (λ x, P))
(at level 1, format "{[ x | P ]}") : C_scope.
(at level 1, format "{[ x | P ]}") : stdpp_scope.
Instance set_elem_of {A} : ElemOf A (set A) := λ x X, set_car X x.
......
......@@ -13,7 +13,7 @@ Notation length := List.length.
(** * Fix scopes *)
Open Scope string_scope.
Open Scope list_scope.
Infix "+:+" := String.append (at level 60, right associativity) : C_scope.
Infix "+:+" := String.append (at level 60, right associativity) : stdpp_scope.
Arguments String.append : simpl never.
(** * Decision of equality *)
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment