diff options
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index b622543..32f507d 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -86,9 +86,6 @@ Require Import ssrfun ssrbool eqtype ssrnat. (* ** Filtering: *) (* filter p s == the subsequence of s consisting of all the items *) (* for which the (boolean) predicate p holds. *) -(* subfilter s : seq sT == when sT has a subType p structure, the sequence *) -(* of items of type sT corresponding to items of s *) -(* for which p holds. *) (* rem x s == the subsequence of s, where the first occurrence *) (* of x has been removed (compare filter (predC1 x) s *) (* where ALL occurrences of x are removed). *) |