Commit 123a7c05 authored by Robbert Krebbers's avatar Robbert Krebbers

Big ops over gmap without binder for the key.

parent 562b2c2b
......@@ -44,6 +44,9 @@ Typeclasses Opaque big_opM.
Notation "'[⋅' 'map' ] k ↦ x ∈ m , P" := (big_opM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[⋅ map ] k ↦ x ∈ m , P") : C_scope.
Notation "'[⋅' 'map' ] x ∈ m , P" := (big_opM m (λ _ x, P))
(at level 200, m at level 10, x at level 1, right associativity,
format "[⋅ map ] x ∈ m , P") : C_scope.
Definition big_opS {M : ucmraT} `{Countable A}
(X : gset A) (f : A M) : M := [] (f <$> elements X).
......
......@@ -47,6 +47,9 @@ Typeclasses Opaque uPred_big_sepM.
Notation "'[★' 'map' ] k ↦ x ∈ m , P" := (uPred_big_sepM m (λ k x, P))
(at level 200, m at level 10, k, x at level 1, right associativity,
format "[★ map ] k ↦ x ∈ m , P") : uPred_scope.
Notation "'[★' 'map' ] x ∈ m , P" := (uPred_big_sepM m (λ _ x, P))
(at level 200, m at level 10, x at level 1, right associativity,
format "[★ map ] x ∈ m , P") : uPred_scope.
Definition uPred_big_sepS {M} `{Countable A}
(X : gset A) (Φ : A uPred M) : uPred M := [] (Φ <$> elements X).
......
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