Commit 0c4e2984 authored by Robbert Krebbers's avatar Robbert Krebbers

Clearify `(pat1 & pat2 & .. & patn)` syntax.

parent 5fa04408
Pipeline #19114 passed with stage
in 14 minutes and 43 seconds
...@@ -216,6 +216,8 @@ _introduction patterns_: ...@@ -216,6 +216,8 @@ _introduction patterns_:
+ Either the proposition `P` or `Q` should be persistent. + Either the proposition `P` or `Q` should be persistent.
+ Either `ipat1` or `ipat2` should be `_`, which results in one of the + Either `ipat1` or `ipat2` should be `_`, which results in one of the
conjuncts to be thrown away. conjuncts to be thrown away.
- `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
to eliminate nested (separating) conjunctions.
- `[ipat1|ipat2]` : disjunction elimination. - `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination. - `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously). - `%` : move the hypothesis to the pure Coq context (anonymously).
......
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