Commit 33ca3791 authored by Robbert's avatar Robbert

Merge branch 'docs' into 'master'

Updating the ProofMode.md docs

See merge request !53
parents 3d6525a5 54e7671c
...@@ -57,7 +57,7 @@ Introduction of logical connectives ...@@ -57,7 +57,7 @@ Introduction of logical connectives
----------------------------------- -----------------------------------
- `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals - `iPureIntro` : turn a pure goal into a Coq goal. This tactic works for goals
of the shape `■ φ`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs. of the shape `⌜φ⌝`, `a ≡ b` on discrete COFEs, and `✓ a` on discrete CMRAs.
- `iLeft` : left introduction of disjunction. - `iLeft` : left introduction of disjunction.
- `iRight` : right introduction of disjunction. - `iRight` : right introduction of disjunction.
...@@ -113,7 +113,7 @@ Modalities ...@@ -113,7 +113,7 @@ Modalities
---------- ----------
- `iModIntro` : introduction of a modality that is an instance of the - `iModIntro` : introduction of a modality that is an instance of the
`IntoModal` type class. Instances include: later, except 0, basic update and `FromModal` type class. Instances include: later, except 0, basic update and
fancy update. fancy update.
- `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,
......
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