SeqFilter

Functions for removing elements of a sequence by a predicate on data.

Signature of SeqFilter

List of Import References :
See BOOL
See DENOTATION
See Nat
See Option
See Seq

SIGNATURE SeqFilter[data]

$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)

Parameter

SORT data

Imports

IMPORT Seq[data] ONLY seq
       Seq[seq[data]] ONLY seq

Filter functions

p | s: filter, select all elements of s fulfilling predicate p.

FUN |           : (data -> bool) ** seq[data] -> seq[data]      

Long name for | with and without currying

FUN filter  : (data -> bool) ** seq[data] -> seq[data]
FUN filter  : (data -> bool) -> seq[data] -> seq[data]

-- @code{partition (p, s) = (p | s, (\\x. ~(p(x))) | s)}
FUN partition   : (data -> bool) ** seq[data] -> seq[data] ** seq[data]

take (p, s1) = s2: take all components of s1 (from left to right) fulfilling predicate p just upto the first component, which does not fulfill p.

FUN take        : (data -> bool) ** seq[data] -> seq[data]      

drop (p, s1) = s2: drop all components of s1 (from left to right) fulfilling predicate p just upto the first component, which does not fulfill p.

FUN drop        : (data -> bool) ** seq[data] -> seq[data]      
                

split (p, s) = (take (p,s), drop (p, s)): split s before the first component (operating from left to right) which does not fulfill predicate p.

FUN split       : (data -> bool) ** seq[data] -> seq[data] ** seq[data] 

components(~)(s) = s0 :: s1 :: ... :: sn. s = s0 ++ s1 ++ ..., all elements of si are related by ~, and the last element of si is not related by ~ with si+1

FUN components: (data ** data -> bool) -> seq[data] -> seq[seq[data]]

next node: SeqFold,
prev node: SeqConv,
up to node: Subsystem Sequences Proper