next node: SetByBSTFold,
prev node: SetByBSTConv,
up to node: Subsystem Sets By Binary Search Trees


SetByBSTFilter

This structure contains functions for filtering of sets

Signature of SetByBSTFilter

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

Parameter

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

Filtering

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