Skip to content

GitLab

Commit ad0201e9 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files
Options

Fix typo in ProofMode.md (thanks to Hai).

parent 219cc3a9
Hide whitespace changes
Inline Side-by-side
Showing with 2 additions and 2 deletions
ProofMode.md
View file @ ad0201e9
...@@ -41,8 +41,8 @@ Context management ...@@ -41,8 +41,8 @@ Context management
the resulting goal. the resulting goal.
- `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and - `iPoseProof pm_trm as (x1 ... xn) "ipat"` : put `pm_trm` into the context and
eliminates it. This tactic is essentially the same as `iDestruct` with the eliminates it. This tactic is essentially the same as `iDestruct` with the
difference that when `pm_trm` is a non-univerisally quantified spatial difference that when `pm_trm` is a non-univerisally quantified persistent
hypothesis, it will not throw the hypothesis away. hypothesis, it will not throw away the hypothesis.
- `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the - `iAssert P with "spat" as "ipat"` : generates a new subgoal `P` and adds the
hypothesis `P` to the current goal. The specialization pattern `spat` hypothesis `P` to the current goal. The specialization pattern `spat`
specifies which hypotheses will be consumed by proving `P`. The introduction specifies which hypotheses will be consumed by proving `P`. The introduction
......
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