more

XintaoYu · Jan 15, 2024 · 0518f3e · 0518f3e
1 parent b22cf8d
commit 0518f3e
Show file tree

Hide file tree

Showing 10 changed files with 14 additions and 27 deletions.
diff --git a/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean b/EuclideanGeometry/Foundation/Axiom/Linear/Line.lean
@@ -1,4 +1,4 @@
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 import EuclideanGeometry.Foundation.Axiom.Linear.Ray
 
 noncomputable section

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean b/EuclideanGeometry/Foundation/Axiom/Position/Angle_ex2.lean
@@ -1,5 +1,5 @@
 import EuclideanGeometry.Foundation.Axiom.Position.Angle
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 
 noncomputable section
 

diff --git a/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean b/EuclideanGeometry/Foundation/Axiom/Position/Orientation.lean
@@ -1,4 +1,4 @@
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
 import EuclideanGeometry.Foundation.Axiom.Position.Angle
 import EuclideanGeometry.Foundation.Axiom.Position.Angle_trash

diff --git a/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean b/EuclideanGeometry/Foundation/Axiom/Triangle/Basic.lean
@@ -1,5 +1,5 @@
 import EuclideanGeometry.Foundation.Axiom.Position.Orientation
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 
 universe u
 

diff --git a/EuclideanGeometry/Foundation/Index.lean b/EuclideanGeometry/Foundation/Index.lean
@@ -6,7 +6,7 @@ import EuclideanGeometry.Foundation.Axiom.Basic.Class
 /- Axiom.Linear -/
 import EuclideanGeometry.Foundation.Axiom.Linear.Ray
 import EuclideanGeometry.Foundation.Axiom.Linear.Ray_trash
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 import EuclideanGeometry.Foundation.Axiom.Linear.Line
 import EuclideanGeometry.Foundation.Axiom.Linear.Class
 import EuclideanGeometry.Foundation.Axiom.Linear.Parallel
@@ -40,7 +40,7 @@ import EuclideanGeometry.Foundation.Axiom.Circle.CirclePower
 import EuclideanGeometry.Foundation.Tactic.Congruence.Attr
 import EuclideanGeometry.Foundation.Tactic.Congruence.Congruence
 -- import EuclideanGeometry.Foundation.Tactic.Congruence.Congruence' -- `need to avoid some name collision during initialization?`
-import EuclideanGeometry.Foundation.Tactic.Colinear.perm_collinear
+import EuclideanGeometry.Foundation.Tactic.Collinear.perm_collinear
 
 /- Constuction -/
 import EuclideanGeometry.Foundation.Construction.Inversion

diff --git a/...dation/Tactic/Colinear/perm_colinear.lean → ...tion/Tactic/Collinear/perm_collinear.lean b/...dation/Tactic/Colinear/perm_colinear.lean → ...tion/Tactic/Collinear/perm_collinear.lean
@@ -1,21 +1,21 @@
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 
 namespace EuclidGeom
 
 open Lean Lean.Meta Lean.Elab Lean.Elab.Tactic Qq
 
 variable {P : Type _} [EuclideanPlane P]
 
-def extractColinear (expr : Q(Prop)) : MetaM (Option Expr) :=
+def extractCollinear (expr : Q(Prop)) : MetaM (Option Expr) :=
   match expr with
   | ~q(@EuclidGeom.collinear _ (_) _ _ _) =>
       return .some expr
   | _ => return .none
 
-def getColinearDeclNames : TacticM (List Name) := withMainContext do
+def getCollinearDeclNames : TacticM (List Name) := withMainContext do
   flip (<- getLCtx).foldlM [] fun acc x => do
     let type := x.type
-    pure $ match <- (extractColinear type) with
+    pure $ match <- (extractCollinear type) with
     | .some _ => x.userName :: acc
     | .none => acc
 
@@ -25,7 +25,7 @@ syntax (name := perm_collinear) "perm_collinear"  : tactic
 def evalPerm_collinear : Tactic := fun stx =>
   match stx with
   | `(tactic| perm_collinear) => withTheReader Term.Context ({· with errToSorry := false }) do
-    let collinearDeclNames <- getColinearDeclNames
+    let collinearDeclNames <- getCollinearDeclNames
     for x0 in collinearDeclNames do
       let x0 := mkIdent x0
       try

diff --git a/EuclideanGeometry/Unused/Line.lean b/EuclideanGeometry/Unused/Line.lean
@@ -1,4 +1,4 @@
-import EuclideanGeometry.Foundation.Axiom.Linear.Colinear
+import EuclideanGeometry.Foundation.Axiom.Linear.Collinear
 
 noncomputable section
 namespace EuclidGeom

diff --git a/Plan_files/DetailedPlan/Axiom-Linear.txt b/Plan_files/DetailedPlan/Axiom-Linear.txt
@@ -339,7 +339,7 @@ Theorem
 \end{itemize}
 
 
-\section{Content in file Colinear.lean}
+\section{Content in file Collinear.lean}
 
 In this section, We discuss colinarity of points on a plane.
 

diff --git a/Plan_files/Plan.lean b/Plan_files/Plan.lean
@@ -8,7 +8,7 @@ Axiom Folder
 
   subfolder : Linear
     Ray -- Define segments and rays (including midpoint here)
-    Colinear -- Define colinarity
+    Collinear -- Define collinearity
     Line -- Define lines, define the class LinObj and unify their toProj
     Parallel -- Define parallel lines and basic properties
     Perpendicular -- Define the perpendicular lines and perpendicular foot

diff --git a/lakefile.lean b/lakefile.lean
@@ -1,26 +1,13 @@
 import Lake
 open Lake DSL
 
-def moreServerArgs := #[
-  "-Dpp.unicode.fun=true", -- pretty-prints `fun a ↦ b`
-  "-Dpp.proofs.withType=false",
-  "-DautoImplicit=false",
-  "-DrelaxedAutoImplicit=false"
-]
-
-def moreLeanArgs := moreServerArgs
-
 package EG where
-  moreServerArgs := moreServerArgs
-  moreLeanArgs := moreLeanArgs
-/- for leanprover/lean4:v4.4.0-rc1
   leanOptions := #[
     ⟨`pp.unicode.fun, true⟩, -- pretty-prints `fun a ↦ b`
     ⟨`pp.proofs.withType, false⟩,
     ⟨`autoImplicit, false⟩,
     ⟨`relaxedAutoImplicit, false⟩
   ]
--/
 
 @[default_target]
 lean_lib «EuclideanGeometry» {