This structure contains functions for filtering of sets
List of Import References :
See BOOL
See BSTree
See DENOTATION
See Nat
See Option
See Pair
See Seq
See SetByBST
See Tree
SIGNATURE SetByBSTFilter[data,< :data ** data -> bool]
$Date: 2010-09-30 18:24:17 +0200 (Do, 30. Sep 2010) $ ($Revision: 616 $)
IMPORT SetByBST[data, <] ONLY set
data
is the element type, <
is a total strict
order: the formula ALL x y. ~(x < y) AND ~(y < x) => x === y must
hold.
SORT data FUN < : data ** data -> bool
Filter: select all elements of the set fulfilling the predicate.
FUN | : (data -> bool) ** set -> set
In partition (p, s) == (s1,s2)
, s1
contains that
elements of s
which fulfill p
, s2
contains those
elements which donot fulfill p
.
FUN partition: (data -> bool) ** set -> set ** set
next node: SetByBSTFold,
prev node: SetByBSTConv,
up to node: Subsystem Sets By Binary Search Trees