diff options
| -rw-r--r-- | doc/refman/Cases.tex | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/refman/Cases.tex b/doc/refman/Cases.tex index 7ad895f9d8..376ef031db 100644 --- a/doc/refman/Cases.tex +++ b/doc/refman/Cases.tex @@ -280,6 +280,18 @@ Fail Check end). \end{coq_example} +The option {\tt Set Asymmetric Patterns} \optindex{Asymmetric Patterns} +(off by default) removes parameters from constructors in patterns: +\begin{coq_example} + Set Asymmetric Patterns. + Check (fun l:List nat => + match l with + | nil => nil + | cons _ l' => l' + end) + Unset Asymmetric Patterns. +\end{coq_example} + \paragraph{Implicit arguments in patterns} By default, implicit arguments are omitted in patterns. So we write: |