% @(#)$Id: day_of_week_Trait.lsl,v 1.6 1997/06/03 20:29:59 leavens Exp $
day_of_week_Trait: trait
  includes int, NoContainedObjects(day_of_week)
  introduces
    sun, mon, tues, wed, thurs, fri, sat: -> day_of_week
    to_int: day_of_week -> int

  asserts
    day_of_week generated by sun, mon, tues, wed, thurs, fri, sat
    day_of_week partitioned by to_int: day_of_week -> int
    equations
      to_int(sun) == 1;
      to_int(mon) == 2;
      to_int(tues) == 3;
      to_int(wed) == 4;
      to_int(thurs) == 5;
      to_int(fri) == 6;
      to_int(sat) == 7;

  implies
    \forall d1, d2: day_of_week
      (d1 = d2) == (to_int(d1) = to_int(d2))
      converts to_int: day_of_week -> int

[Index]

HTML generated using lcpp2html.