% @(#)$Id: with_member_objs.lsl,v 1.4 1995/08/23 22:58:34 leavens Exp $
% This trait is useful for defining contained_objects for generic containers,
% such as Set<T>, List<T>, etc, for which the trait function \in is defined.
% See container_objs for a stronger trait that assumes more.

with_member_objs(E,C): trait
  includes contained_objects(C)
  assumes HasMembership(E,C), contained_objects(E)
  asserts
    \forall e: E, c: C, st: State
      (e \in c)
         => (contained_objects(e,st) \subseteq contained_objects(c, st))

[Index]

HTML generated using lcpp2html.