% @(#)$Id: IgnoringTypeTags.lsl,v 1.1 1995/11/09 23:08:47 leavens Exp $
IgnoringTypeTags(TYPE): trait
  assumes TypeTaggedObject(TYPE)
  includes Set(Object, Set[Object], int for Int),
           Set(TypeTaggedObject, Set[TypeTaggedObject], int for Int)
  introduces 
    ignoringTypeTags: Set[TypeTaggedObject] -> Set[Object]
  asserts
    \forall stto: Set[TypeTaggedObject], tto: TypeTaggedObject
      ignoringTypeTags({}) == {};
      ignoringTypeTags(insert(tto, stto))
        == insert(tto.obj, ignoringTypeTags(stto));

[Index]

HTML generated using lcpp2html.