Verified Commit 3162a652 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso
Browse files

fractional_big_sep*: uniform type annotations

To match the suggestion in
iris/iris!737 (comment 75017).
parent 830e8148
......@@ -77,8 +77,8 @@ Section fractional.
rewrite !assoc. f_equiv. by rewrite comm.
Qed.
Global Instance fractional_big_sepL {A} l Ψ :
( k (x : A), Fractional (Ψ k x))
Global Instance fractional_big_sepL {A} (l : list A) Ψ :
( k x, Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ list] kx l, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepL_sep. by setoid_rewrite fractional. Qed.
......@@ -88,7 +88,7 @@ Section fractional.
Proof. intros ? q q'. rewrite -big_sepL2_sep. by setoid_rewrite fractional. Qed.
Global Instance fractional_big_sepM `{Countable K} {A} (m : gmap K A) Ψ :
( k (x : A), Fractional (Ψ k x))
( k x, Fractional (Ψ k x))
Fractional (PROP:=PROP) (λ q, [ map] kx m, Ψ k x q)%I.
Proof. intros ? q q'. rewrite -big_sepM_sep. by setoid_rewrite fractional. Qed.
......
Supports Markdown
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