diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2015-11-05 16:04:59 +0100 |
|---|---|---|
| committer |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 09:35:16 +0100 |
| commit | 7028d08eb6e08d1a1af7f8e99f2e9edd880b8da2 (patch) | |
| tree | 7e79b41d89f119059292bfe93d37f229a726cb1f /doc/refman | |
| parent | 435c8b0fdf3c01d2618d1ffbbfe2321250326420 (diff) | |
ENH: improving precision
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 148c4505c..f6e9152ca 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -1295,7 +1295,7 @@ one corresponds to object $m$. \Coq{} can sometimes infer this predicate but sometimes not. The concrete syntax for describing this predicate uses the \kw{as\ldots in\ldots return} construction. For instance, let us assume that $I$ is an unary predicate with one -parameter. The predicate is made explicit using the syntax: +parameter and one argument. The predicate is made explicit using the syntax: \[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ P ~\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}\] |