Details About PVS Vectors Library

  IMPORTING vectors,         % N-dimensional vectors and operations
            vectors_rew,     % Adds distributive rewrites
                             % See strategies (vect-distr) (vect-distr-off) 
            vect2D,          % Define 2-D Vector from N-dimensional vectors
            vect3D,          % Define 3-D Vector from N-dimensional vectors

            vectors2D,       % 2-dimensional vectors and operations
            vectors2D_rew,   % Adds distributive rewrites
                             % See strategies (vect-distr) (vect-distr-off) 

            vectors3D,       % 3-dimensional vectors and operations
            vectors3D_rew,   % Adds distributive rewrites
                             % See strategies (vect-distr) (vect-distr-off) 

            vectors_cos,     % Law of cosines for n-D vectors 
            vectors2D_cos,   % Law of cosines for 2D vectors 
            vectors3D_cos,   % Law of cosines for 3D vectors 

            position,        % using vectors for position, distance function
            position2D,      % using vectors for 2D-position, distance function
            position3D,      % using vectors for 3D-position, distance function

            lines,           % Using vectors to define lines, and motion
            lines2D,         % Using vectors to define lines, and motion
            lines3D,         % Using vectors to define lines, and motion

            law_cos_pos2D,   % Law of cosines for 2D positions 
            law_cos_pos3D,   % Law of cosines for 3D positions 

            closest_approach,      %% NEW %%   
            closest_approach_2D,   %% NEW %%
            closest_approach_3D,   %% NEW %%

            perpendicular2D, % line perpendicular to a line through a point
            perpendicular3D, % line perpendicular to a line through a point

            vectors_sign2D,  % signs of vector dot product    

            intersections2D, %   %% NEW %% finding intersection points of lines

            matrices,        % Theory of matrices

WITH

   zero: vector = (LAMBDA i: 0) ;

   -(v): vector = (LAMBDA i: -v(i)) ;

   +(u,v)(i): real = u(i) + v(i) ;
   -(u,v)(i): real = u(i) - v(i) ;

   *(u,v): real = sigma(1,Dim,(LAMBDA i: u(i)*v(i))) ;
   *(a,v): vector = (LAMBDA i: a*v(i))