From c2b2ea2dce5fa7b8d428a5072f2e86979eeb1d98 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Sat, 21 Nov 2020 13:30:45 +0900 Subject: Apply suggestions from code review Co-authored-by: Christian Doczkal --- mathcomp/ssreflect/seq.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'mathcomp/ssreflect') 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]. *) -- cgit v1.2.3