From 39f9137700784ea80ab34d5eefdc1a4da04fb0ad Mon Sep 17 00:00:00 2001
From: James <jamesgallicchio@gmail.com>
Date: Sat, 8 Jun 2024 17:25:14 -0400
Subject: [PATCH] reword

---
 ITP/geometry.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/ITP/geometry.tex b/ITP/geometry.tex
index 452970b..47d8128 100644
--- a/ITP/geometry.tex
+++ b/ITP/geometry.tex
@@ -16,7 +16,7 @@
 def ConvexEmptyIn (S P : Set Point) : Prop :=
     ConvexIndep S ∧ EmptyShapeIn S P
 
-/-- `HasEmptyKGon k P' means that `P' has a convex `k'-gon in `P' -/
+/-- `HasEmptyKGon k P' means that `P' has a convex, empty `k'-gon -/
 def HasEmptyKGon (k : Nat) (P : Set Point) : Prop :=
     ∃ S : Finset Point, S.card = k ∧ ↑S ⊆ P ∧ ConvexEmptyIn S P
 \end{lstlisting}