Commit e4f1b5c2 authored by Robbert Krebbers's avatar Robbert Krebbers

A bunch of missing Params instances.

parent 686f5740
......@@ -193,7 +193,7 @@ Section list_theory.
Context `(R' : relation B) (f : A B) {Hf: Proper (R ==> R') f}.
Collection Hyps := Type Hf.
Local Set Default Proof Using "Hyps".
Global Instance list_setincl_fmap :
Proper (list_setincl R ==> list_setincl R') (fmap f).
Proof using Hf.
......@@ -201,7 +201,7 @@ Section list_theory.
destruct (Hab _ Ha) as (b & Hb & HR). exists (f b).
split; first eapply elem_of_list_fmap; eauto.
Qed.
Global Instance list_setequiv_fmap :
Proper (list_setequiv R ==> list_setequiv R') (fmap f).
Proof using Hf. intros ?? [??]. split; apply list_setincl_fmap; done. Qed.
......@@ -213,9 +213,7 @@ Section list_theory.
intros (a & -> & Ha)%elem_of_list_fmap (b & -> & Hb)%elem_of_list_fmap.
apply Hf. exact: Hl.
Qed.
End fmap.
End list_theory.
Section agree.
......@@ -408,6 +406,7 @@ Lemma agree_validI {M} x y : ✓ (x ⋅ y) ⊢ (x ≡ y : uPred M).
Proof. uPred.unseal; split=> r n _ ?; by apply: agree_op_invN. Qed.
End agree.
Instance: Params (@to_agree) 1.
Arguments agreeC : clear implicits.
Arguments agreeR : clear implicits.
......
......@@ -10,13 +10,17 @@ Local Arguments cmra_validN _ _ !_ /.
Local Arguments cmra_valid _ !_ /.
Inductive csum (A B : Type) :=
| Cinl : A csum A B
| Cinr : B csum A B
| CsumBot : csum A B.
| Cinl : A csum A B
| Cinr : B csum A B
| CsumBot : csum A B.
Arguments Cinl {_ _} _.
Arguments Cinr {_ _} _.
Arguments CsumBot {_ _}.
Instance: Params (@Cinl) 2.
Instance: Params (@Cinr) 2.
Instance: Params (@CsumBot) 2.
Instance maybe_Cinl {A B} : Maybe (@Cinl A B) := λ x,
match x with Cinl a => Some a | _ => None end.
Instance maybe_Cinr {A B} : Maybe (@Cinr A B) := λ x,
......
......@@ -10,6 +10,9 @@ Inductive excl (A : Type) :=
Arguments Excl {_} _.
Arguments ExclBot {_}.
Instance: Params (@Excl) 1.
Instance: Params (@ExclBot) 1.
Notation excl' A := (option (excl A)).
Notation Excl' x := (Some (Excl x)).
Notation ExclBot' := (Some ExclBot).
......
......@@ -422,6 +422,8 @@ Notation "p .1" := (fst p) (at level 10, format "p .1").
Notation "p .2" := (snd p) (at level 10, format "p .2").
Instance: Params (@pair) 2.
Instance: Params (@fst) 2.
Instance: Params (@snd) 2.
Notation curry := prod_curry.
Notation uncurry := prod_uncurry.
......
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