Commit 461c88d6 authored by Robbert Krebbers's avatar Robbert Krebbers

And more useless new lines.

parent 1a5d7d58
Pipeline #24338 failed with stage
in 18 minutes and 38 seconds
......@@ -108,17 +108,13 @@ Separation logic-specific tactics
- `iFrame (t1 .. tn) "selpat"` : cancel the Coq terms (or Coq hypotheses)
`t1 ... tn` and Iris hypotheses given by `selpat` in the goal. The constructs
of the selection pattern have the following meaning:
+ `%` : repeatedly frame hypotheses from the Coq context.
+ `#` : repeatedly frame hypotheses from the intuitionistic context.
+ `∗` : frame as much of the spatial context as possible. (N.B: this
is the unicode symbol `∗`, not the regular asterisk `*`.)
Notice that framing spatial hypotheses makes them disappear, but framing Coq
or intuitionistic hypotheses does not make them disappear.
This tactic solves the goal if everything in the conclusion has been
framed.
This tactic solves the goal if everything in the conclusion has been framed.
- `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.
- `iAccu` : solves a goal that is an evar by instantiating it with a all
......@@ -176,7 +172,6 @@ Rewriting / simplification
goal / hypotheses given by the selection pattern `selpat`. This is a
shorthand for `iEval (simpl)`.
Iris
----
......
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