Merge pull request #6 from bsubercaseaux/orientation-comment

remove comments on orientation def
bsubercaseaux · Jun 10, 2024 · 4983f58 · 4983f58
2 parents 5218720 + 843b44e
commit 4983f58
Show file tree

Hide file tree

Showing 2 changed files with 9 additions and 6 deletions.
diff --git a/ITP/triple-orientations.tex b/ITP/triple-orientations.tex
@@ -104,9 +104,9 @@
 % @[pp_dot] abbrev y (p : Point) : ℝ := p 1
 \begin{lstlisting}
 inductive Orientation : Type where
-  | cw -- clockwise :=  -
-  | ccw -- counter clockwise := +
-  | collinear -- := 0
+  | cw          -- Clockwise turn
+  | ccw         -- Counter-clockwise turn
+  | collinear   -- Collinear
 
 noncomputable def σ (p q r : Point) : Orientation :=
   let det := Matrix.det !![p.x, q.x, r.x ; p.y, q.y, r.y ; 1, 1, 1]

diff --git a/Lean/Geo/Definitions/Orientations.lean b/Lean/Geo/Definitions/Orientations.lean
@@ -12,9 +12,12 @@ noncomputable section
 open Classical
 
 inductive Orientation : Type where
-  | cw -- clockwise :=  -
-  | ccw -- counter clockwise := +
-  | collinear -- := 0
+  /-- 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
 
 def Orientation.neg : Orientation → Orientation