diff options
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. *) (******************************************************************************) |