From ceb9fa1f88afc2cda4a4477c208a3ca4bfda08a3 Mon Sep 17 00:00:00 2001 From: Robbert Krebbers <mail@robbertkrebbers.nl> Date: Tue, 29 Sep 2020 13:28:51 +0200 Subject: [PATCH] Improve docs for `iModIntro`. Based om https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/467#note_53064 by @Blaisorblade. --- docs/proof_mode.md | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/docs/proof_mode.md b/docs/proof_mode.md index dca9f23df..6e9cdbaac 100644 --- a/docs/proof_mode.md +++ b/docs/proof_mode.md @@ -131,8 +131,12 @@ Modalities used to specify which modalities this tactic should introduce. Instances of that type class include: later, except 0, basic update and fancy update, intuitionistically, persistently, affinely, plainly, absorbingly, objectively, - and subjectively. The optional argument `mod` can be used to specify what - modality to introduce in case of ambiguity, e.g. `⎡|==> P⎤`. + and subjectively. The optional argument `mod` is a term pattern (i.e., a term + with holes as underscores). If present, `iModIntro` will find a subterm + matching `mod`, and try introducing its topmost modality. For instance, if the + goal is `⎡|==> P⎤`, using `iModIntro ⎡|==> P⎤%I` or `iModIntro ⎡_⎤%I` would + introduce `⎡_⎤` and produce goal `|==> P`, while `iModIntro (|==> _)%I` would + introduce `|==>` and produce goal `⎡P⎤`. - `iAlways` : a deprecated alias of `iModIntro`. - `iNext n` : an alias of `iModIntro (▷^n _)`. - `iNext` : an alias of `iModIntro (▷^_ _)`. -- GitLab