% @(#)$Id: FourSidedFigure.lsl,v 1.7 1997/08/01 04:40:13 leavens Exp $
FourSidedFigure(Scalar): trait

  includes PreVector(Scalar, Vector for Vec[T]), int,
           Val_Array(Vector)

  introduces
    isLoop: Arr[Vector] -> Bool
    \<__,__,__,__\>: Vector, Vector, Vector, Vector -> Arr[Vector]

  asserts
   \forall e: Arr[Vector], v1,v2,v3,v4:Vector
     isLoop(e) == (e[0] + e[1] + e[2] + e[3] = 0:Vector);
     \<v1,v2,v3,v4\>
        == assign(assign(assign(assign(create(4), 0,v1), 1,v2), 2,v3),
                  3,v4);

  implies
   \forall e: Arr[Vector], v1,v2,v3,v4:Vector
      size(\<v1,v2,v3,v4\>) == 4;
      (\<v1,v2,v3,v4\>)[0] == v1;
      (\<v1,v2,v3,v4\>)[1] == v2;
      (\<v1,v2,v3,v4\>)[2] == v3;
      (\<v1,v2,v3,v4\>)[3] == v4;
      allAllocated(\<v1,v2,v3,v4\>);
   converts
     isLoop:Arr[Vector] -> Bool,
     \<__,__,__,__\>: Vector, Vector, Vector, Vector -> Arr[Vector]

[Index]

HTML generated using lcpp2html.