| generic | |
| type T_horizontal is new float; | |
| -- Declaration of types, constants, and common functions on 3D vectors. | |
| -- Corresponds to PVS theory vectors/vectors_2D | |
| package Aspect1_Vectors_2D is | |
| -- A 2D vector, represented by an x and a y coordinate. | |
| type Vect2 is record | |
| x: T_horizontal; | |
| y: T_horizontal; | |
| end record; | |
| subtype Nz_vect2 is Vect2 | |
| with Predicate => (Nz_vect2.x /= 0.0 and then Nz_Vect2.y /= 0.0); | |
| end Aspect1_Vectors_2D; |