diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 15:42:17 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:15 +0100 |
| commit | 0ad9953cfacda53dea9b08f3b5b60ee5531b0850 (patch) | |
| tree | bb42b51212104838d06113b3cc8cbaa67a0f04f2 /doc/refman | |
| parent | d95fd157ac6600f4784de44ef558c4880aed624b (diff) | |
CLEANUP: removing duplicate paragraph
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index f69b40278..bea0079a5 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1277,12 +1277,6 @@ $m$ in an inductive type $I$ and we want to prove a property which possibly depends on $m$. For this, it is enough to prove the property for $m = (c_i~u_1\ldots u_{p_i})$ for each constructor of $I$. - -The basic idea of this operator is that we have an object -$m$ in an inductive type $I$ and we want to prove a property -which possibly depends on $m$. For this, it is enough to prove the -property for $m = (c_i~u_1\ldots u_{p_i})$ for each constructor of $I$. - The \Coq{} term for this proof will be written: \[\kw{match}~m~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~ (c_n~x_{n1}~...~x_{np_n}) \Ra f_n~ \kw{end}\] |