From 0c4e2984e5bf5db86c5123cc5cc255b71737d410 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 16 Aug 2019 10:08:19 +0200
Subject: [PATCH] Clearify `(pat1 & pat2 & .. & patn)` syntax.
---
ProofMode.md | 2 ++
1 file changed, 2 insertions(+)
diff --git a/ProofMode.md b/ProofMode.md
index fe780136f..5014c1958 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -216,6 +216,8 @@ _introduction patterns_:
+ Either the proposition `P` or `Q` should be persistent.
+ Either `ipat1` or `ipat2` should be `_`, which results in one of the
conjuncts to be thrown away.
+- `(pat1 & pat2 & ... & patn)` : syntactic sugar for `[pat1 [pat2 .. patn ..]]`
+ to eliminate nested (separating) conjunctions.
- `[ipat1|ipat2]` : disjunction elimination.
- `[]` : false elimination.
- `%` : move the hypothesis to the pure Coq context (anonymously).
--
GitLab