add doc comments to Orientation code

bsubercaseaux · Jun 8, 2024 · e54df20 · e54df20
1 parent c5ebeed
commit e54df20
Showing 1 changed file with 3 additions and 0 deletions.
diff --git 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