% @(#)$Id: IsaRhombus.lsl,v 1.4 1997/07/25 22:49:22 leavens Exp $
IsaRhombus: trait
  includes IsaParallelogram
  introduces
    isaRhombus: Arr[Vector] -> Bool
  asserts
    \forall e: Arr[Vector]
      isaRhombus(e) == isaParallelogram(e)
                       /\ (length(e[0]) = length(e[1]));
  implies
    \forall e: Arr[Vector]
      isaRhombus(e) => isaParallelogram(e);
      isaRhombus(e) == isaParallelogram(e)
                       /\ (length(e[0]) = length(e[2]));
      isaRhombus(e) == isaParallelogram(e)
                       /\ (length(e[0]) = length(e[3]));

[Index]

HTML generated using lcpp2html.