% $Id: RelSet.html,v 1.1 2003/10/01 07:22:16 connolly Exp $
% larch Set trait is for finite sets

RelSet(E, C): trait
    includes
        Relation(E, C,
                  __ \< __ \> __ for __ 〈 __ 〉 __,
                 bot for ⊥, top for ⊤)

    introduces
        { __ } : E → C
        { } : → C

    asserts
        ∀ e1, e2: E, c: C
        {} = bot;
        e1 ∈ { e2 } ⇔ (e1 = e2);

[Index]

HTML generated using lsl2html.