diff options
| author | Cyril Cohen | 2017-09-07 17:14:29 +0200 |
|---|---|---|
| committer | GitHub | 2017-09-07 17:14:29 +0200 |
| commit | 5a08a2a78f35de41f099a3bd1a49908591d02729 (patch) | |
| tree | 66bf6d04a453bc880db25fb986b870bfa7d90531 | |
| parent | 1597073304060566a2949ccd9e9ea49ab2deca9c (diff) | |
| parent | 3c20f9049d4881a9f16404929e5d135b9ef23ee6 (diff) | |
Merge pull request #106 from akr/remove-subfilter-doc
remove documentation for subfilter.
| -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). *) |