diff options
| author | Antonio Nikishaev | 2020-04-05 02:54:23 +0400 |
|---|---|---|
| committer | Antonio Nikishaev | 2020-04-08 01:13:13 +0400 |
| commit | 815d3cbfa2bf98b4b8f2bcd14819a20eca843e78 (patch) | |
| tree | d3564d7ccb62b38493fde1a0fc23ff94410074ec /mathcomp/ssreflect/bigop.v | |
| parent | 14e28e78155e3e6cfbe78aee0964569283f04d7d (diff) | |
fix typos in documentation: text
Diffstat (limited to 'mathcomp/ssreflect/bigop.v')
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 6d18825..698f2e7 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -5,12 +5,12 @@ From mathcomp Require Import div fintype tuple finfun. (******************************************************************************) (* This file provides a generic definition for iterating an operator over a *) -(* set of indices (bigop); this big operator is parametrized by the return *) +(* set of indices (bigop); this big operator is parameterized by the return *) (* type (R), the type of indices (I), the operator (op), the default value on *) (* empty lists (idx), the range of indices (r), the filter applied on this *) (* range (P) and the expression we are iterating (F). The definition is not *) (* to be used directly, but via the wide range of notations provided and *) -(* and which support a natural use of big operators. *) +(* which support a natural use of big operators. *) (* To improve performance of the Coq typechecker on large expressions, the *) (* bigop constant is OPAQUE. It can however be unlocked to reveal the *) (* transparent constant reducebig, to let Coq expand summation on an explicit *) @@ -27,7 +27,7 @@ From mathcomp Require Import div fintype tuple finfun. (* 2. Results depending on the properties of the operator: *) (* We distinguish: monoid laws (op is associative, idx is an identity *) (* element), abelian monoid laws (op is also commutative), and laws with *) -(* a distributive operation (semi-rings). Examples of such results are *) +(* a distributive operation (semirings). Examples of such results are *) (* splitting, permuting, and exchanging bigops. *) (* A special section is dedicated to big operators on natural numbers. *) (******************************************************************************) |