Skip to content
Snippets Groups Projects
Commit 462b056f authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Fix typos in docs of `iNext`.

parent 3091e4d4
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 2 additions and 2 deletions
docs/proof_mode.md
+ 2
− 2
View file @ 462b056f
...@@ -134,8 +134,8 @@ Modalities ...@@ -134,8 +134,8 @@ Modalities
and subjectively. The optional argument `mod` can be used to specify what and subjectively. The optional argument `mod` can be used to specify what
modality to introduce in case of ambiguity, e.g. `⎡|==> P⎤`. modality to introduce in case of ambiguity, e.g. `⎡|==> P⎤`.
- `iAlways` : a deprecated alias of `iModIntro`. - `iAlways` : a deprecated alias of `iModIntro`.
- `iNext n` : an alias of `iModIntro (▷^n P)`. - `iNext n` : an alias of `iModIntro (▷^n _)`.
- `iNext` : an alias of `iModIntro (▷^1 P)`. - `iNext` : an alias of `iModIntro (▷^_ _)`.
- `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is - `iMod pm_trm as (x1 ... xn) "ipat"` : eliminate a modality `pm_trm` that is
an instance of the `ElimModal` type class. Instances include: later, except 0, an instance of the `ElimModal` type class. Instances include: later, except 0,
basic update and fancy update. basic update and fancy update.
......
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