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

[Index]

HTML generated using lcpp2html.