Commit 9b53243c authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typo.

parent a15dc76f
...@@ -521,7 +521,7 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP) ...@@ -521,7 +521,7 @@ Definition accessor {PROP : bi} {X : Type} (M1 M2 : PROP → PROP)
(α β : X PROP) (mγ : X option PROP) : PROP := (α β : X PROP) (mγ : X option PROP) : PROP :=
M1 ( x, α x (β x - M2 (default emp (mγ x))))%I. M1 ( x, α x (β x - M2 (default emp (mγ x))))%I.
(* Typeclass for assertions around which accessors can be elliminated. (* Typeclass for assertions around which accessors can be eliminated.
Inputs: [Q], [E1], [E2], [α], [β], [γ] Inputs: [Q], [E1], [E2], [α], [β], [γ]
Outputs: [Q'] Outputs: [Q']
......
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