From e54df209e8b08404852045aacf3ef2f5bd1d4ccc Mon Sep 17 00:00:00 2001
From: James <jamesgallicchio@gmail.com>
Date: Sat, 8 Jun 2024 16:59:33 -0400
Subject: [PATCH] add doc comments to Orientation code

---
 Lean/Geo/Definitions/Orientations.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Lean/Geo/Definitions/Orientations.lean b/Lean/Geo/Definitions/Orientations.lean
index 7b7f56b..2aac863 100644
--- a/Lean/Geo/Definitions/Orientations.lean
+++ b/Lean/Geo/Definitions/Orientations.lean
@@ -12,8 +12,11 @@ noncomputable section
 open Classical
 
 inductive Orientation : Type where
+  /-- Clockwise turn; `det x y z < 0` -/
   | cw
+  /-- Counter-clockwise turn; `det x y z > 0` -/
   | ccw
+  /-- Collinear; `det x y z = 0` -/
   | collinear
   deriving DecidableEq, Repr