Commit 1b5e1bc6 authored by Ralf Jung's avatar Ralf Jung
Browse files

use tc_opaque for a complicated definition

parent 15fd682e
Pipeline #66084 passed with stage
in 8 minutes and 18 seconds
......@@ -35,10 +35,10 @@ Section box_defs.
box_own_prop γ P inv N (slice_inv γ P).
Definition box (f : gmap slice_name bool) (P : iProp Σ) : iProp Σ :=
Φ : slice_name iProp Σ,
tc_opaque ( Φ : slice_name iProp Σ,
(P [ map] γ _ f, Φ γ)
[ map] γ b f, box_own_auth γ (E b) box_own_prop γ (Φ γ)
inv N (slice_inv γ (Φ γ)).
inv N (slice_inv γ (Φ γ)))%I.
End box_defs.
Global Instance: Params (@box_own_prop) 3 := {}.
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