Skip to content

GitLab

Commit 60d28bbb authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Document `iAccu`.

parent 9d8af00a
Show whitespace changes
Inline Side-by-side
ProofMode.md
View file @ 60d28bbb
...@@ -111,6 +111,9 @@ Separation logic-specific tactics ...@@ -111,6 +111,9 @@ Separation logic-specific tactics
framed. framed.
- `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into - `iCombine "H1" "H2" as "pat"` : combines `H1 : P1` and `H2 : P2` into
`H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis. `H: P1 ∗ P2`, then calls `iDestruct H as pat` on the combined hypothesis.
- `iAccu` : solves a goal that is an evar by instantiating it with a all
hypotheses from the spatial context joined together with a separating
conjunction (or `emp` in case the spatial context is empty).
Modalities Modalities
---------- ----------
......
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