next node: SetFilter,
prev node: Set,
up to node: Subsystem Sets Proper


SetConv

Functions for converting sets to seqneces or textual represenatation.

Signature of SetConv

List of Import References :
See BOOL
See Char
See DENOTATION
See Nat
See Option
See Seq
See Set
See String

SIGNATURE SetConv[data,< :data ** data -> bool]

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

IMPORT  Set[data, <]  ONLY set
        Seq[data]     ONLY seq
        String        ONLY string

Parameter

SORT data
FUN <   : data**data->bool
 

total strict-order; in D ~(x < y) AND ~(y < x) => x = y should = represent semantic equality.

Converting from and to Seqences

asSet(<e0, e1, ..., en>) == {e0, e1, ..., en} handles duplicate members in seq

FUN asSet: seq -> set    

asSeq({e0, e1, ..., en}) == <e0, e1, ..., en> order may vary since order in sets does not matter.

FUN asSeq: set -> seq

Textual Representation

`(f)({e0, e1, ..., en}) == "{" f(e0) "," f(e1) "," ... "," f(en) "}"

FUN ` : (data -> denotation) -> set -> denotation
FUN ` : (data -> string)     -> set -> string

The additional parameters correspond to open brace, comma and close brace repectively.

FUN ` : (denotation ** denotation ** denotation) ->
         (data -> denotation) -> set -> denotation
FUN ` : (denotation ** denotation ** denotation) ->
         (data -> string)     -> set -> string


next node: SetFilter,
prev node: Set,
up to node: Subsystem Sets Proper