A non-degenerate polygon is a tuple consisting of a natural number \(n \ge 3\), a function \(V : \mathrm{Fin}\, n \to \mathbb {Q}^2\) giving the vertices in counterclockwise order, and a proof that \(V\) is injective.

A convex polygon is a non-degenerate polygon in which, for every directed edge \(V_i \to V_{i+1}\), every other vertex lies strictly to the left of the edge. Strictness excludes collinear triples and therefore makes every vertex an extreme point of the convex hull of \(\{ V_i\} \).

Each edge of a convex polygon defines a closed half-space weakly to its left; the polygon coincides with the intersection of these half-spaces.

A point lies in a convex polygon iff it lies in every edge half-space. A convex polygon \(P\) is a subset of \(Q\) iff every vertex of \(P\) lies in \(Q\).

The function convexHullRationalPoints returns, from a finite list of rational points, a list of extreme points in counterclockwise order starting at the lexicographically smallest point. ConvexPolygon.ofList upgrades this to an Option ConvexPolygon, returning none when fewer than three extreme points remain.

Given a list of closed half-spaces, the convex polygon defined by their intersection is obtained by taking all pairwise boundary intersections and retaining those satisfying every half-space constraint.

Given \(d, \tau {\gt} 0\), one shrinks a convex polygon by moving each edge inward by an amount in \([d, d + \tau ]\) and intersecting the resulting half-spaces. The output is an Option ConvexPolygon, since the result may be empty.

The area of a convex polygon with vertex list \((V_0, \ldots , V_{n-1})\) is