Commit 226b8579 authored by Robbert Krebbers's avatar Robbert Krebbers

Add proof mode documentation for the `-# pat` intro pattern.

parent 25061957
...@@ -240,6 +240,10 @@ _introduction patterns_: ...@@ -240,6 +240,10 @@ _introduction patterns_:
hypothesis is already in the intuitionistic context, the tactic will still hypothesis is already in the intuitionistic context, the tactic will still
strip intuitionistic and persistence modalities (it is a no-op if the strip intuitionistic and persistence modalities (it is a no-op if the
hypothesis does not contain such modalities). hypothesis does not contain such modalities).
- `-# ipat` : move the hypothesis from the intuitionistic context into the
spatial context. If the hypothesis is already in the spatial context, the
tactic is a no-op. If the hypothesis is not affine, an `<affine>` modality is
added to the hypothesis.
- `> ipat` : eliminate a modality (if the goal permits). - `> ipat` : eliminate a modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only Apart from this, there are the following introduction patterns that can only
......
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