% $Id: RelSet.lsl,v 1.2 2000/01/17 21:33:40 connolly Exp $
% larch Set trait is for finite sets

RelSet(E, C): trait
    includes
        Relation(E, C,
                  __ \< __ \> __ for __ á __ ñ __,
                 bot for \bot, top for \top)

    introduces
        { __ } : E ® C
        { } : ® C

    asserts
        " e1, e2: E
        (e1 \< { e2 } \> e1) = (e1=e2);
        e1 \notin {};


[Index]

[source]

HTML generated using lsl2html.