diff options
| author | Kazuhiko Sakaguchi | 2020-11-21 13:30:45 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-11-25 22:29:54 +0900 |
| commit | c2b2ea2dce5fa7b8d428a5072f2e86979eeb1d98 (patch) | |
| tree | f2c02c36d18ee3841e07db4c8f35c99bed6f4284 /mathcomp | |
| parent | 783631c771ec76baa4ff9d292c1eddfb58f67f4c (diff) | |
Apply suggestions from code review
Co-authored-by: Christian Doczkal <christian.doczkal@inria.fr>
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index c3936bb..777041f 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -133,8 +133,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. (* [seq f x y | x <- s, y <- t] *) (* := [:: f x_1 y_1; ...; f x_1 y_m; f x_2 y_1; ...; f x_n y_m] *) (* allrel r xs ys := all [pred x | all (r x) ys] xs *) -(* == the proposition r x y holds for all x and y respectively *) -(* in xs and ys. *) +(* == r x y holds whenever x is in xs and y is in ys *) (* all1rel r xs := allrel r xs xs *) (* == the proposition r x y holds for all possible x, y in xs. *) (* map f s == the sequence [:: f x_1, ..., f x_n]. *) |