plangeo4 plangeo4.ocd 2006-06-01 experimental 2004-06-01 0 4 This CD defines symbols for planar Euclidean geometry. In particular, it is concerned with projective and affine coordinates of points and lines. set_coordinates This symbol defines the coordinates of a point or a line. The coordinates are the projective coordinates and consist of a vector of length 3. Points whose third coordinates are zero are the points at infinity. The line whose first two coordinates are zero is the line at infinity. 1 2 3 coordinates This function yields the coordinates vector if applied to a point or line with coordinates. 1 1 2 2 3 3 To extract the coordinates of a point A with coordinates (1,2,3): 1 2 3 is_affine Boolean function testing whether a point or line is affine. 3 1 2 affine_coordinates This function yields the affine coordinates vector if applied to a point or line with coordinates in the affine plane. The affine coordinates (1/3,2/3) are expressed as follows for the point A with projective coordinates (1,2,3). 1 2 3 set_affine_coordinates Defines the affine coordinates of an affine point or line. Assign the affine coordinates (1/3,2/3) to A. 1 3 2 3