diff options
| author | Yves Bertot | 2020-11-20 11:26:57 +0100 |
|---|---|---|
| committer | Yves Bertot | 2020-11-20 11:26:57 +0100 |
| commit | 8aa783e1a4fb0f5c759d297f015686b7a1f99ed6 (patch) | |
| tree | fd6dae8a9e98d65f0ae53ec828562f1e25ea2b3a | |
| parent | b4cdd47bcd7f2b2f9033ee00b7412570b07b8808 (diff) | |
typo in documentation of allpairs_dep
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index c658ac2..3d56831 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -126,7 +126,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* s and t, respectively, in row-major order, *) (* and where t is possibly dependent in elements of s *) (* allpairs_dep f s t := self expanding definition for *) -(* [seq f x y | x <- s, y <- t i] *) +(* [seq f x y | x <- s, y <- t y] *) (* ** Iterators: for s == [:: x_1, ..., x_n], t == [:: y_1, ..., y_m], *) (* allpairs f s t := same as allpairs_dep but where t is non dependent, *) (* i.e. self expanding definition for *) |
