% @(#)$Id: TypeTag.lsl,v 1.4 1995/11/10 06:46:58 leavens Exp $
TypeTag(T): trait
  assumes State, WidenNarrow(T, Object)
  includes TypeTaggedObject, IgnoringTypeTags,
           SortNames(T, TYPE, type_of for sort_of)
  introduces
    asTypeTaggedObject: T -> TypeTaggedObject
  asserts
    \forall o: T
      asTypeTaggedObject(o) == [widen(o), type_of(o)];
  implies
    \forall o: T
      asTypeTaggedObject(o).obj == widen(o);

[Index]

HTML generated using lcpp2html.