Commit 3f7f9f4e authored by Robbert Krebbers's avatar Robbert Krebbers

Update example in ProofMode.md

parent 60d28bbb
......@@ -237,11 +237,13 @@ appear at the top level:
For example, given:
∀ x, x = 0 ⊢ □ (P → False ∨ □ (Q ∧ ▷ R) -∗ P ∗ ▷ (R ∗ Q ∧ x = pred 2)).
∀ x, <affine> ⌜ x = 0 ⌝ ⊢
□ (P → False ∨ □ (Q ∧ ▷ R) -∗
P ∗ ▷ (R ∗ Q ∧ ⌜ x = pred 2 ⌝)).
You can write
iIntros (x) "% !# $ [[] | #[HQ HR]] /= !>".
iIntros (x Hx) "!# $ [[] | #[HQ HR]] /= !>".
which results in:
......
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