% @(#)$Id: color_Trait.lsl,v 1.6 1997/06/03 20:29:59 leavens Exp $
color_Trait: trait
  includes int, NoContainedObjects(color)
  introduces
    red, orange, yellow, green, blue, indigo, violet: -> color
    to_int: color -> int

  asserts
    color generated by red, orange, yellow, green, blue, indigo, violet
    color partitioned by to_int: color -> int
    equations
      to_int(red) == 0;
      to_int(orange) == 1;
      to_int(yellow) == 2;
      to_int(green) == 3;
      to_int(blue) == 4;
      to_int(indigo) == 5;
      to_int(violet) == 5;

  implies
    \forall c1, c2: color
      (c1 = c2) == (to_int(c1) = to_int(c2))
    converts to_int: color -> int

[Index]

HTML generated using lcpp2html.