chore: use _eq instead of eq to name auto generated equational theorems

src/Lean/Elab/PreDefinition/Eqns.lean

@@ -111,7 +111,7 @@ builtin_initialize eqnsExt : EnvExtension EqnsExtState ←
 
 /-- Create a "unique" base name for equations and splitter -/
 def mkBaseNameFor (env : Environment) (declName : Name) : Name :=
-  Lean.mkBaseNameFor env declName `eq_1 `_eqns
+  Lean.mkBaseNameFor env declName `_eq_1 `_eqns
 
 /-- Try to close goal using `rfl` with smart unfolding turned off. -/
 def tryURefl (mvarId : MVarId) : MetaM Bool :=

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -64,7 +64,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.structural.eqns] "{eqnTypes[i]}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof info.declName type
     addDecl <| Declaration.thmDecl {

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -72,7 +72,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
   for i in [: eqnTypes.size] do
     let type := eqnTypes[i]
     trace[Elab.definition.wf.eqns] "{eqnTypes[i]}"
-    let name := baseName ++ (`eq).appendIndexAfter (i+1)
+    let name := baseName ++ (`_eq).appendIndexAfter (i+1)
     thmNames := thmNames.push name
     let value ← mkProof declName type
     addDecl <| Declaration.thmDecl {

tests/lean/run/structuralEqns.lean

@@ -6,8 +6,8 @@ def tst (declName : Name) : MetaM Unit := do
   IO.println (← getEqnsFor? declName)
 
 #eval tst ``List.map
-#check @List.map.eq_1
-#check @List.map.eq_2
+#check @List.map._eq_1
+#check @List.map._eq_2
 
 def foo (xs ys zs : List Nat) : List Nat :=
   match (xs, ys) with
@@ -20,8 +20,8 @@ def foo (xs ys zs : List Nat) : List Nat :=
 
 #eval tst ``foo
 
-#check foo.eq_1
-#check foo.eq_2
+#check foo._eq_1
+#check foo._eq_2
 
 #eval tst ``foo
 
@@ -33,11 +33,11 @@ def g : List Nat → List Nat → Nat
   | x::xs,      []    => g xs []
 
 #eval tst ``g
-#check g.eq_1
-#check g.eq_2
-#check g.eq_3
-#check g.eq_4
-#check g.eq_5
+#check g._eq_1
+#check g._eq_2
+#check g._eq_3
+#check g._eq_4
+#check g._eq_5
 
 def h (xs : List Nat) (y : Nat) : Nat :=
   match xs with
@@ -48,9 +48,9 @@ def h (xs : List Nat) (y : Nat) : Nat :=
     | y+1 => h xs y
 
 #eval tst ``h
-#check h.eq_1
-#check h.eq_2
-#check h.eq_3
+#check h._eq_1
+#check h._eq_2
+#check h._eq_3
 
 def r (i j : Nat) : Nat :=
   i +
@@ -62,9 +62,9 @@ def r (i j : Nat) : Nat :=
           | Nat.succ j => r i j
 
 #eval tst ``r
-#check r.eq_1
-#check r.eq_2
-#check r.eq_3
+#check r._eq_1
+#check r._eq_2
+#check r._eq_3
 
 def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α :=
   f i <|
@@ -76,6 +76,6 @@ def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α :=
           | Nat.succ j => bla f g a i j
 
 #eval tst ``bla
-#check @bla.eq_1
-#check @bla.eq_2
-#check @bla.eq_3
+#check @bla._eq_1
+#check @bla._eq_2
+#check @bla._eq_3

tests/lean/run/structuralEqns2.lean

@@ -12,9 +12,9 @@ def g (i j : Nat) : Nat :=
   | Nat.succ j => g i j
 
 #eval tst ``g
-#check g.eq_1
-#check g.eq_2
-#check g.eq_3
+#check g._eq_1
+#check g._eq_2
+#check g._eq_3
 
 def h (i j : Nat) : Nat :=
   let z :=
@@ -24,5 +24,5 @@ def h (i j : Nat) : Nat :=
   z + z
 
 #eval tst ``h
-#check h.eq_1
-#check h.eq_2
+#check h._eq_1
+#check h._eq_2

tests/lean/run/structuralEqns3.lean

@@ -15,5 +15,5 @@ def wk_comp : Wk n m → Wk m l → Wk n l
 
 #eval tst ``wk_comp
 
-#check @wk_comp.eq_1
-#check @wk_comp.eq_2
+#check @wk_comp._eq_1
+#check @wk_comp._eq_2

tests/lean/run/wfEqns1.lean

@@ -23,5 +23,5 @@ decreasing_by
 #print isEven
 
 #eval tst ``isEven
-#check @isEven.eq_1
-#check @isEven.eq_2
+#check @isEven._eq_1
+#check @isEven._eq_2

tests/lean/run/wfEqns2.lean

@@ -31,9 +31,9 @@ decreasing_by
     decide
 
 #eval tst ``g
-#check g.eq_1
-#check g.eq_2
-#check g.eq_3
+#check g._eq_1
+#check g._eq_2
+#check g._eq_3
 #eval tst ``h
-#check h.eq_1
-#check h.eq_2
+#check h._eq_1
+#check h._eq_2

tests/lean/run/wfEqns3.lean

@@ -16,4 +16,4 @@ decreasing_by
   exact h
 
 #eval tst ``f
-#check f.eq_1
+#check f._eq_1

tests/lean/run/wfEqns4.lean

@@ -36,9 +36,9 @@ decreasing_by
 #eval f 5 'a' 'b'
 
 #eval tst ``f
-#check @f.eq_1
-#check @f.eq_2
+#check @f._eq_1
+#check @f._eq_2
 
 #eval tst ``h
-#check @h.eq_1
-#check @h.eq_2
+#check @h._eq_1
+#check @h._eq_2